Commit 2025-01-22 09:03 c971e4ff

View on Github →

feat: a non-zero constant function is integrable iff the measure is finite (#20914) The situation here is that I want to case on IsFiniteMeasure μ, and in the negative branch I want to get ¬ Integrable (fun _ ↦ c) μ. The current lemma integrable_const_iff is not very useful for that. From my PhD (LeanCamCombi)

Estimated changes