Commit 2025-01-29 18:12 f6cd2928

View on Github →

chore(MeasureTheory/Function/L1Space): split L1Space into HasFiniteIntegral, Integrable and AEEqFun (#21231) Split the too long file L1Space into three files:

HasFiniteIntegral contains the corresponding predicate and associated lemmas.
Integrable contains the corresponding predicate and associated lemmas.
AEEqFun links the Integrable predicate with the L1 space α →₁[μ] β.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

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

added theorem MeasureTheory.AEEqFun.Integrable.add

added theorem MeasureTheory.AEEqFun.Integrable.neg

added theorem MeasureTheory.AEEqFun.Integrable.smul

added theorem MeasureTheory.AEEqFun.Integrable.sub

added def MeasureTheory.AEEqFun.Integrable

added theorem MeasureTheory.AEEqFun.integrable_coeFn

added theorem MeasureTheory.AEEqFun.integrable_iff_mem_L1

added theorem MeasureTheory.AEEqFun.integrable_mk

added theorem MeasureTheory.AEEqFun.integrable_zero

added theorem MeasureTheory.Integrable.coeFn_toL1

added theorem MeasureTheory.Integrable.edist_toL1_toL1

added theorem MeasureTheory.Integrable.edist_toL1_zero

added theorem MeasureTheory.Integrable.enorm_toL1

added theorem MeasureTheory.Integrable.norm_toL1

added theorem MeasureTheory.Integrable.norm_toL1_eq_lintegral_norm

added def MeasureTheory.Integrable.toL1

added theorem MeasureTheory.Integrable.toL1_add

added theorem MeasureTheory.Integrable.toL1_coeFn

added theorem MeasureTheory.Integrable.toL1_eq_mk

added theorem MeasureTheory.Integrable.toL1_eq_toL1_iff

added theorem MeasureTheory.Integrable.toL1_neg

added theorem MeasureTheory.Integrable.toL1_smul'

added theorem MeasureTheory.Integrable.toL1_smul

added theorem MeasureTheory.Integrable.toL1_sub

added theorem MeasureTheory.Integrable.toL1_zero

added theorem MeasureTheory.L1.aemeasurable_coeFn

added theorem MeasureTheory.L1.aestronglyMeasurable_coeFn

added theorem MeasureTheory.L1.dist_def

added theorem MeasureTheory.L1.edist_def

added theorem MeasureTheory.L1.hasFiniteIntegral_coeFn

added theorem MeasureTheory.L1.integrable_coeFn

added theorem MeasureTheory.L1.measurable_coeFn

added theorem MeasureTheory.L1.norm_def

added theorem MeasureTheory.L1.norm_sub_eq_lintegral

added theorem MeasureTheory.L1.ofReal_norm_eq_lintegral

added theorem MeasureTheory.L1.ofReal_norm_sub_eq_lintegral

added theorem MeasureTheory.L1.stronglyMeasurable_coeFn

Created Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean

added theorem MeasureTheory.HasFiniteIntegral.add_measure

added theorem MeasureTheory.HasFiniteIntegral.congr'

added theorem MeasureTheory.HasFiniteIntegral.congr

added theorem MeasureTheory.HasFiniteIntegral.const_mul

added theorem MeasureTheory.HasFiniteIntegral.left_of_add_measure

added theorem MeasureTheory.HasFiniteIntegral.max_zero

added theorem MeasureTheory.HasFiniteIntegral.min_zero

added theorem MeasureTheory.HasFiniteIntegral.mono'

added theorem MeasureTheory.HasFiniteIntegral.mono

added theorem MeasureTheory.HasFiniteIntegral.mono_measure

added theorem MeasureTheory.HasFiniteIntegral.mul_const

added theorem MeasureTheory.HasFiniteIntegral.neg

added theorem MeasureTheory.HasFiniteIntegral.norm

added theorem MeasureTheory.HasFiniteIntegral.of_finite

added theorem MeasureTheory.HasFiniteIntegral.of_mem_Icc

added theorem MeasureTheory.HasFiniteIntegral.restrict

added theorem MeasureTheory.HasFiniteIntegral.right_of_add_measure

added theorem MeasureTheory.HasFiniteIntegral.smul

added theorem MeasureTheory.HasFiniteIntegral.smul_measure

added def MeasureTheory.HasFiniteIntegral

added theorem MeasureTheory.all_ae_ofReal_F_le_bound

added theorem MeasureTheory.all_ae_ofReal_f_le_bound

added theorem MeasureTheory.all_ae_tendsto_ofReal_norm

added theorem MeasureTheory.hasFiniteIntegral_add_measure

added theorem MeasureTheory.hasFiniteIntegral_congr'

added theorem MeasureTheory.hasFiniteIntegral_congr

added theorem MeasureTheory.hasFiniteIntegral_const

added theorem MeasureTheory.hasFiniteIntegral_const_iff

added theorem MeasureTheory.hasFiniteIntegral_const_iff_isFiniteMeasure

added theorem MeasureTheory.hasFiniteIntegral_count_iff

added theorem MeasureTheory.hasFiniteIntegral_def

added theorem MeasureTheory.hasFiniteIntegral_iff_edist

added theorem MeasureTheory.hasFiniteIntegral_iff_enorm

added theorem MeasureTheory.hasFiniteIntegral_iff_norm

added theorem MeasureTheory.hasFiniteIntegral_iff_ofNNReal

added theorem MeasureTheory.hasFiniteIntegral_iff_ofReal

added theorem MeasureTheory.hasFiniteIntegral_neg_iff

added theorem MeasureTheory.hasFiniteIntegral_norm_iff

added theorem MeasureTheory.hasFiniteIntegral_of_bounded

added theorem MeasureTheory.hasFiniteIntegral_of_dominated_convergence

added theorem MeasureTheory.hasFiniteIntegral_smul_iff

added theorem MeasureTheory.hasFiniteIntegral_toReal_iff

added theorem MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top

added theorem MeasureTheory.hasFiniteIntegral_zero

added theorem MeasureTheory.hasFiniteIntegral_zero_measure

added theorem MeasureTheory.isFiniteMeasure_withDensity_ofReal

added theorem MeasureTheory.lintegral_edist_triangle

added theorem MeasureTheory.lintegral_enorm_add_left

added theorem MeasureTheory.lintegral_enorm_add_right

added theorem MeasureTheory.lintegral_enorm_eq_lintegral_edist

added theorem MeasureTheory.lintegral_enorm_neg

added theorem MeasureTheory.lintegral_enorm_zero

added theorem MeasureTheory.lintegral_norm_eq_lintegral_edist

added theorem MeasureTheory.tendsto_lintegral_norm_of_dominated_convergence

Renamed Mathlib/MeasureTheory/Function/L1Space.lean to Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

deleted theorem MeasureTheory.AEEqFun.Integrable.add

deleted theorem MeasureTheory.AEEqFun.Integrable.neg

deleted theorem MeasureTheory.AEEqFun.Integrable.smul

deleted theorem MeasureTheory.AEEqFun.Integrable.sub

deleted def MeasureTheory.AEEqFun.Integrable

deleted theorem MeasureTheory.AEEqFun.integrable_coeFn

deleted theorem MeasureTheory.AEEqFun.integrable_iff_mem_L1

deleted theorem MeasureTheory.AEEqFun.integrable_mk

deleted theorem MeasureTheory.AEEqFun.integrable_zero

deleted theorem MeasureTheory.HasFiniteIntegral.add_measure

deleted theorem MeasureTheory.HasFiniteIntegral.congr'

deleted theorem MeasureTheory.HasFiniteIntegral.congr

deleted theorem MeasureTheory.HasFiniteIntegral.const_mul

deleted theorem MeasureTheory.HasFiniteIntegral.left_of_add_measure

deleted theorem MeasureTheory.HasFiniteIntegral.max_zero

deleted theorem MeasureTheory.HasFiniteIntegral.min_zero

deleted theorem MeasureTheory.HasFiniteIntegral.mono'

deleted theorem MeasureTheory.HasFiniteIntegral.mono

deleted theorem MeasureTheory.HasFiniteIntegral.mono_measure

deleted theorem MeasureTheory.HasFiniteIntegral.mul_const

deleted theorem MeasureTheory.HasFiniteIntegral.neg

deleted theorem MeasureTheory.HasFiniteIntegral.norm

deleted theorem MeasureTheory.HasFiniteIntegral.of_finite

deleted theorem MeasureTheory.HasFiniteIntegral.of_mem_Icc

deleted theorem MeasureTheory.HasFiniteIntegral.restrict

deleted theorem MeasureTheory.HasFiniteIntegral.right_of_add_measure

deleted theorem MeasureTheory.HasFiniteIntegral.smul

deleted theorem MeasureTheory.HasFiniteIntegral.smul_measure

deleted def MeasureTheory.HasFiniteIntegral

deleted theorem MeasureTheory.Integrable.coeFn_toL1

deleted theorem MeasureTheory.Integrable.edist_toL1_toL1

deleted theorem MeasureTheory.Integrable.edist_toL1_zero

deleted theorem MeasureTheory.Integrable.enorm_toL1

deleted theorem MeasureTheory.Integrable.norm_toL1

deleted theorem MeasureTheory.Integrable.norm_toL1_eq_lintegral_norm

deleted def MeasureTheory.Integrable.toL1

deleted theorem MeasureTheory.Integrable.toL1_add

deleted theorem MeasureTheory.Integrable.toL1_coeFn

deleted theorem MeasureTheory.Integrable.toL1_eq_mk

deleted theorem MeasureTheory.Integrable.toL1_eq_toL1_iff

deleted theorem MeasureTheory.Integrable.toL1_neg

deleted theorem MeasureTheory.Integrable.toL1_smul'

deleted theorem MeasureTheory.Integrable.toL1_smul

deleted theorem MeasureTheory.Integrable.toL1_sub

deleted theorem MeasureTheory.Integrable.toL1_zero

deleted theorem MeasureTheory.L1.aemeasurable_coeFn

deleted theorem MeasureTheory.L1.aestronglyMeasurable_coeFn

deleted theorem MeasureTheory.L1.dist_def

deleted theorem MeasureTheory.L1.edist_def

deleted theorem MeasureTheory.L1.hasFiniteIntegral_coeFn

deleted theorem MeasureTheory.L1.integrable_coeFn

deleted theorem MeasureTheory.L1.measurable_coeFn

deleted theorem MeasureTheory.L1.norm_def

deleted theorem MeasureTheory.L1.norm_sub_eq_lintegral

deleted theorem MeasureTheory.L1.ofReal_norm_eq_lintegral

deleted theorem MeasureTheory.L1.ofReal_norm_sub_eq_lintegral

deleted theorem MeasureTheory.L1.stronglyMeasurable_coeFn

deleted theorem MeasureTheory.all_ae_ofReal_F_le_bound

deleted theorem MeasureTheory.all_ae_ofReal_f_le_bound

deleted theorem MeasureTheory.all_ae_tendsto_ofReal_norm

deleted theorem MeasureTheory.hasFiniteIntegral_add_measure

deleted theorem MeasureTheory.hasFiniteIntegral_congr'

deleted theorem MeasureTheory.hasFiniteIntegral_congr

deleted theorem MeasureTheory.hasFiniteIntegral_const

deleted theorem MeasureTheory.hasFiniteIntegral_const_iff

deleted theorem MeasureTheory.hasFiniteIntegral_const_iff_isFiniteMeasure

deleted theorem MeasureTheory.hasFiniteIntegral_count_iff

deleted theorem MeasureTheory.hasFiniteIntegral_def

deleted theorem MeasureTheory.hasFiniteIntegral_iff_edist

deleted theorem MeasureTheory.hasFiniteIntegral_iff_enorm

deleted theorem MeasureTheory.hasFiniteIntegral_iff_norm

deleted theorem MeasureTheory.hasFiniteIntegral_iff_ofNNReal

deleted theorem MeasureTheory.hasFiniteIntegral_iff_ofReal

deleted theorem MeasureTheory.hasFiniteIntegral_neg_iff

deleted theorem MeasureTheory.hasFiniteIntegral_norm_iff

deleted theorem MeasureTheory.hasFiniteIntegral_of_bounded

deleted theorem MeasureTheory.hasFiniteIntegral_of_dominated_convergence

deleted theorem MeasureTheory.hasFiniteIntegral_smul_iff

deleted theorem MeasureTheory.hasFiniteIntegral_toReal_iff

deleted theorem MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top

deleted theorem MeasureTheory.hasFiniteIntegral_zero

deleted theorem MeasureTheory.hasFiniteIntegral_zero_measure

deleted theorem MeasureTheory.isFiniteMeasure_withDensity_ofReal

deleted theorem MeasureTheory.lintegral_edist_triangle

deleted theorem MeasureTheory.lintegral_enorm_add_left

deleted theorem MeasureTheory.lintegral_enorm_add_right

deleted theorem MeasureTheory.lintegral_enorm_eq_lintegral_edist

deleted theorem MeasureTheory.lintegral_enorm_neg

deleted theorem MeasureTheory.lintegral_enorm_zero

deleted theorem MeasureTheory.lintegral_norm_eq_lintegral_edist

deleted theorem MeasureTheory.tendsto_lintegral_norm_of_dominated_convergence

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Modified Mathlib/MeasureTheory/Function/UnifTight.lean

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

Modified Mathlib/Probability/Independence/Integrable.lean

Modified Mathlib/Probability/Moments/IntegrableExpMul.lean