Commit 2023-06-02 12:29 151c25bc

View on Github →

feat: port MeasureTheory.Integral.SetToL1 (#4579)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/SetToL1.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.L1.SimpleFunc.norm_eq_sum_mul

added theorem MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le'

added theorem MeasureTheory.L1.SimpleFunc.norm_setToL1SCLM_le

added theorem MeasureTheory.L1.SimpleFunc.norm_setToL1S_le

added def MeasureTheory.L1.SimpleFunc.setToL1S

added def MeasureTheory.L1.SimpleFunc.setToL1SCLM'

added def MeasureTheory.L1.SimpleFunc.setToL1SCLM

added theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left'

added theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left

added theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left'

added theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left

added theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_measure

added theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_const

added theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono

added theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left'

added theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_mono_left

added theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_nonneg

added theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left'

added theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left

added theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left'

added theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_add

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_add_left'

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_add_left

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_congr

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_congr_left

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_congr_measure

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_const

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_eq_setToSimpleFunc

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_indicatorConst

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_mono

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_mono_left'

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_mono_left

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_neg

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_nonneg

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul_left'

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul_left

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_smul_real

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_sub

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_zero_left'

added theorem MeasureTheory.L1.SimpleFunc.setToL1S_zero_left

added theorem MeasureTheory.L1.norm_setToL1_le'

added theorem MeasureTheory.L1.norm_setToL1_le

added theorem MeasureTheory.L1.norm_setToL1_le_mul_norm'

added theorem MeasureTheory.L1.norm_setToL1_le_mul_norm

added theorem MeasureTheory.L1.norm_setToL1_le_norm_setToL1SCLM

added theorem MeasureTheory.L1.setToFun_eq_setToL1

added def MeasureTheory.L1.setToL1'

added def MeasureTheory.L1.setToL1

added theorem MeasureTheory.L1.setToL1_add_left'

added theorem MeasureTheory.L1.setToL1_add_left

added theorem MeasureTheory.L1.setToL1_congr_left'

added theorem MeasureTheory.L1.setToL1_congr_left

added theorem MeasureTheory.L1.setToL1_const

added theorem MeasureTheory.L1.setToL1_eq_setToL1'

added theorem MeasureTheory.L1.setToL1_eq_setToL1SCLM

added theorem MeasureTheory.L1.setToL1_indicatorConstLp

added theorem MeasureTheory.L1.setToL1_lipschitz

added theorem MeasureTheory.L1.setToL1_mono

added theorem MeasureTheory.L1.setToL1_mono_left'

added theorem MeasureTheory.L1.setToL1_mono_left

added theorem MeasureTheory.L1.setToL1_nonneg

added theorem MeasureTheory.L1.setToL1_simpleFunc_indicatorConst

added theorem MeasureTheory.L1.setToL1_smul

added theorem MeasureTheory.L1.setToL1_smul_left'

added theorem MeasureTheory.L1.setToL1_smul_left

added theorem MeasureTheory.L1.setToL1_zero_left'

added theorem MeasureTheory.L1.setToL1_zero_left

added theorem MeasureTheory.L1.tendsto_setToL1

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_op_norm

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

added theorem MeasureTheory.continuousAt_setToFun_of_dominated

added theorem MeasureTheory.continuousOn_setToFun_of_dominated

added theorem MeasureTheory.continuousWithinAt_setToFun_of_dominated

added theorem MeasureTheory.continuous_L1_toL1

added theorem MeasureTheory.continuous_setToFun

added theorem MeasureTheory.continuous_setToFun_of_dominated

added theorem MeasureTheory.norm_setToFun_le'

added theorem MeasureTheory.norm_setToFun_le

added theorem MeasureTheory.norm_setToFun_le_mul_norm'

added theorem MeasureTheory.norm_setToFun_le_mul_norm

added def MeasureTheory.setToFun

added theorem MeasureTheory.setToFun_add

added theorem MeasureTheory.setToFun_add_left'

added theorem MeasureTheory.setToFun_add_left

added theorem MeasureTheory.setToFun_congr_ae

added theorem MeasureTheory.setToFun_congr_left'

added theorem MeasureTheory.setToFun_congr_left

added theorem MeasureTheory.setToFun_congr_measure

added theorem MeasureTheory.setToFun_congr_measure_of_add_left

added theorem MeasureTheory.setToFun_congr_measure_of_add_right

added theorem MeasureTheory.setToFun_congr_measure_of_integrable

added theorem MeasureTheory.setToFun_congr_smul_measure

added theorem MeasureTheory.setToFun_const

added theorem MeasureTheory.setToFun_eq

added theorem MeasureTheory.setToFun_finset_sum'

added theorem MeasureTheory.setToFun_finset_sum

added theorem MeasureTheory.setToFun_indicator_const

added theorem MeasureTheory.setToFun_measure_zero'

added theorem MeasureTheory.setToFun_measure_zero

added theorem MeasureTheory.setToFun_mono

added theorem MeasureTheory.setToFun_mono_left'

added theorem MeasureTheory.setToFun_mono_left

added theorem MeasureTheory.setToFun_neg

added theorem MeasureTheory.setToFun_non_aEStronglyMeasurable

added theorem MeasureTheory.setToFun_nonneg

added theorem MeasureTheory.setToFun_smul

added theorem MeasureTheory.setToFun_smul_left'

added theorem MeasureTheory.setToFun_smul_left

added theorem MeasureTheory.setToFun_sub

added theorem MeasureTheory.setToFun_toL1

added theorem MeasureTheory.setToFun_top_smul_measure

added theorem MeasureTheory.setToFun_undef

added theorem MeasureTheory.setToFun_zero

added theorem MeasureTheory.setToFun_zero_left'

added theorem MeasureTheory.setToFun_zero_left

added theorem MeasureTheory.tendsto_setToFun_approxOn_of_measurable

added theorem MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset

added theorem MeasureTheory.tendsto_setToFun_filter_of_dominated_convergence

added theorem MeasureTheory.tendsto_setToFun_of_L1

added theorem MeasureTheory.tendsto_setToFun_of_dominated_convergence