Commit 2025-03-03 13:51 012862cd

View on Github →

feat(MeasureTheory): integrable_tilted_iff (#22435)

Estimated changes

Modified Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

added theorem MeasureTheory.integrable_fun_smul_iff

added theorem MeasureTheory.integrable_withDensity_iff_integrable_smul₀'

Modified Mathlib/MeasureTheory/Measure/Tilted.lean

added theorem MeasureTheory.integrable_tilted_iff