Commit 2025-01-26 17:26 4e9e3115
View on Github →feat: μ[ofNat n * f|m] =ᵐ[μ] ofNat n * μ[f|m]
(#21001)
Also:
- make
condExp_const
a simp lemma - rename
condExp_undef
tocondExp_of_not_integrable
(there are many ways in whichcondExp
is undefined other than the function not being integrable) - specialise
eLpNorm_condExp_le
andMemℒp.condExp
to real inner product spaces as otherwise𝕜
is unconstrained by the return type - add a TODO From my PhD (LeanCamCombi)