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 to condExp_of_not_integrable (there are many ways in which condExp is undefined other than the function not being integrable)
  • specialise eLpNorm_condExp_le and Memℒp.condExp to real inner product spaces as otherwise 𝕜 is unconstrained by the return type
  • add a TODO From my PhD (LeanCamCombi)

Estimated changes