Commit 2025-05-13 15:31 33308ffd

View on Github →

feat(L1Space/Integrable): generalise to enorms (#24820) This covers the first ~600 lines in that file. Most remaining lemmas are for functions into (ENN)Real, or less obvious to generalise.

Estimated changes

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

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

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

modified theorem MeasureTheory.Integrable.add''

modified theorem MeasureTheory.Integrable.add'

modified theorem MeasureTheory.Integrable.add

modified theorem MeasureTheory.Integrable.add_measure

modified theorem MeasureTheory.Integrable.aemeasurable

modified theorem MeasureTheory.Integrable.aestronglyMeasurable

modified theorem MeasureTheory.Integrable.comp_aemeasurable

modified theorem MeasureTheory.Integrable.comp_measurable

added theorem MeasureTheory.Integrable.congr'_enorm

modified theorem MeasureTheory.Integrable.congr

added theorem MeasureTheory.Integrable.enorm

modified theorem MeasureTheory.Integrable.hasFiniteIntegral

modified theorem MeasureTheory.Integrable.left_of_add_measure

added theorem MeasureTheory.Integrable.measure_enorm_ge_lt_top

added theorem MeasureTheory.Integrable.measure_norm_gt_lt_top_enorm

added theorem MeasureTheory.Integrable.mono'_enorm

added theorem MeasureTheory.Integrable.mono_enorm

modified theorem MeasureTheory.Integrable.mono_measure

modified theorem MeasureTheory.Integrable.of_measure_le_smul

added theorem MeasureTheory.Integrable.of_mem_Icc_enorm

modified theorem MeasureTheory.Integrable.right_of_add_measure

modified theorem MeasureTheory.Integrable.smul_measure

modified theorem MeasureTheory.Integrable.smul_measure_nnreal

modified theorem MeasureTheory.Integrable.to_average

modified theorem MeasureTheory.MeasurePreserving.integrable_comp

modified theorem MeasureTheory.MemLp.integrable

added theorem MeasureTheory.MemLp.integrable_enorm_pow'

added theorem MeasureTheory.MemLp.integrable_enorm_pow

added theorem MeasureTheory.MemLp.integrable_enorm_rpow'

added theorem MeasureTheory.MemLp.integrable_enorm_rpow

modified theorem MeasureTheory.integrable_add_measure

modified theorem MeasureTheory.integrable_average

added theorem MeasureTheory.integrable_congr'_enorm

modified theorem MeasureTheory.integrable_congr

added theorem MeasureTheory.integrable_const_enorm

added theorem MeasureTheory.integrable_const_iff_enorm

added theorem MeasureTheory.integrable_const_iff_isFiniteMeasure_enorm

modified theorem MeasureTheory.integrable_dirac'

modified theorem MeasureTheory.integrable_dirac

added theorem MeasureTheory.integrable_enorm_iff

added theorem MeasureTheory.integrable_enorm_rpow_iff

modified theorem MeasureTheory.integrable_finset_sum'

modified theorem MeasureTheory.integrable_finset_sum

modified theorem MeasureTheory.integrable_finset_sum_measure

modified theorem MeasureTheory.integrable_inv_smul_measure

modified theorem MeasureTheory.integrable_map_equiv

modified theorem MeasureTheory.integrable_map_measure

modified theorem MeasureTheory.integrable_of_forall_fin_meas_le

modified theorem MeasureTheory.integrable_smul_measure

modified theorem MeasureTheory.integrable_zero

modified theorem MeasureTheory.integrable_zero_measure

modified theorem MeasureTheory.memLp_one_iff_integrable

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean