Commit 2025-04-15 10:46 bec84036

View on Github →

chore: split MeasureTheory.Integral.SetToL1 (#24075) Move (Dominated)FinMeasAdditive and the lemmas about them to .FinMeasAdditive. This is the last long file to be split.

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean

added theorem MeasureTheory.DominatedFinMeasAdditive.add

added theorem MeasureTheory.DominatedFinMeasAdditive.add_measure_left

added theorem MeasureTheory.DominatedFinMeasAdditive.add_measure_right

added theorem MeasureTheory.DominatedFinMeasAdditive.eq_zero

added theorem MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero

added theorem MeasureTheory.DominatedFinMeasAdditive.of_measure_le

added theorem MeasureTheory.DominatedFinMeasAdditive.of_measure_le_smul

added theorem MeasureTheory.DominatedFinMeasAdditive.of_smul_measure

added theorem MeasureTheory.DominatedFinMeasAdditive.smul

added theorem MeasureTheory.DominatedFinMeasAdditive.zero

added def MeasureTheory.DominatedFinMeasAdditive

added theorem MeasureTheory.FinMeasAdditive.add

added theorem MeasureTheory.FinMeasAdditive.map_empty_eq_zero

added theorem MeasureTheory.FinMeasAdditive.map_iUnion_fin_meas_set_eq_sum

added theorem MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top

added theorem MeasureTheory.FinMeasAdditive.of_smul_measure

added theorem MeasureTheory.FinMeasAdditive.smul

added theorem MeasureTheory.FinMeasAdditive.smul_measure

added theorem MeasureTheory.FinMeasAdditive.smul_measure_iff

added theorem MeasureTheory.FinMeasAdditive.zero

added def MeasureTheory.FinMeasAdditive

added theorem MeasureTheory.SimpleFunc.map_setToSimpleFunc

added theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm

added theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm_of_integrable

added theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm

added def MeasureTheory.SimpleFunc.setToSimpleFunc

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_add

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_add_left'

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_add_left

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_congr'

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_congr

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_congr_left

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_const'

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_const

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_indicator

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left'

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_neg

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg'

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left'

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul_real

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_sub

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_zero'

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_zero

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_zero_apply

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

deleted theorem MeasureTheory.DominatedFinMeasAdditive.add

deleted theorem MeasureTheory.DominatedFinMeasAdditive.add_measure_left

deleted theorem MeasureTheory.DominatedFinMeasAdditive.add_measure_right

deleted theorem MeasureTheory.DominatedFinMeasAdditive.eq_zero

deleted theorem MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero

deleted theorem MeasureTheory.DominatedFinMeasAdditive.of_measure_le

deleted theorem MeasureTheory.DominatedFinMeasAdditive.of_measure_le_smul

deleted theorem MeasureTheory.DominatedFinMeasAdditive.of_smul_measure

deleted theorem MeasureTheory.DominatedFinMeasAdditive.smul

deleted theorem MeasureTheory.DominatedFinMeasAdditive.zero

deleted def MeasureTheory.DominatedFinMeasAdditive

deleted theorem MeasureTheory.FinMeasAdditive.add

deleted theorem MeasureTheory.FinMeasAdditive.map_empty_eq_zero

deleted theorem MeasureTheory.FinMeasAdditive.map_iUnion_fin_meas_set_eq_sum

deleted theorem MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top

deleted theorem MeasureTheory.FinMeasAdditive.of_smul_measure

deleted theorem MeasureTheory.FinMeasAdditive.smul

deleted theorem MeasureTheory.FinMeasAdditive.smul_measure

deleted theorem MeasureTheory.FinMeasAdditive.smul_measure_iff

deleted theorem MeasureTheory.FinMeasAdditive.zero

deleted def MeasureTheory.FinMeasAdditive

deleted theorem MeasureTheory.SimpleFunc.map_setToSimpleFunc

deleted theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm

deleted theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm_of_integrable

deleted theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm

deleted def MeasureTheory.SimpleFunc.setToSimpleFunc

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_add

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_add_left'

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_add_left

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_congr'

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_congr

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_congr_left

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_const'

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_const

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_indicator

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left'

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_neg

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg'

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left'

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_smul_real

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_sub

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_zero'

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_zero

deleted theorem MeasureTheory.SimpleFunc.setToSimpleFunc_zero_apply