Commit 2023-05-31 04:37 27ebbd66

View on Github →

feat: port MeasureTheory.Function.L1Space (#4383)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/L1Space.lean

added theorem ContinuousLinearMap.integrable_comp

added theorem IsUnit.integrable_smul_iff

added theorem MeasurableEmbedding.integrable_map_iff

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.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.right_of_add_measure

added theorem MeasureTheory.HasFiniteIntegral.smul

added theorem MeasureTheory.HasFiniteIntegral.smul_measure

added def MeasureTheory.HasFiniteIntegral

added theorem MeasureTheory.Integrable.abs

added theorem MeasureTheory.Integrable.add'

added theorem MeasureTheory.Integrable.add

added theorem MeasureTheory.Integrable.add_measure

added theorem MeasureTheory.Integrable.aemeasurable

added theorem MeasureTheory.Integrable.aestronglyMeasurable

added theorem MeasureTheory.Integrable.apply_continuousLinearMap

added theorem MeasureTheory.Integrable.bdd_mul'

added theorem MeasureTheory.Integrable.bdd_mul

added theorem MeasureTheory.Integrable.coeFn_toL1

added theorem MeasureTheory.Integrable.comp_aemeasurable

added theorem MeasureTheory.Integrable.comp_measurable

added theorem MeasureTheory.Integrable.congr'

added theorem MeasureTheory.Integrable.congr

added theorem MeasureTheory.Integrable.const_mul'

added theorem MeasureTheory.Integrable.const_mul

added theorem MeasureTheory.Integrable.div_const

added theorem MeasureTheory.Integrable.edist_toL1_toL1

added theorem MeasureTheory.Integrable.edist_toL1_zero

added theorem MeasureTheory.Integrable.essSup_smul

added theorem MeasureTheory.Integrable.hasFiniteIntegral

added theorem MeasureTheory.Integrable.im

added theorem MeasureTheory.Integrable.inf

added theorem MeasureTheory.Integrable.left_of_add_measure

added theorem MeasureTheory.Integrable.measure_ge_lt_top

added theorem MeasureTheory.Integrable.mono'

added theorem MeasureTheory.Integrable.mono

added theorem MeasureTheory.Integrable.mono_measure

added theorem MeasureTheory.Integrable.mul_const'

added theorem MeasureTheory.Integrable.mul_const

added theorem MeasureTheory.Integrable.neg

added theorem MeasureTheory.Integrable.neg_part

added theorem MeasureTheory.Integrable.norm

added theorem MeasureTheory.Integrable.norm_toL1

added theorem MeasureTheory.Integrable.norm_toL1_eq_lintegral_norm

added theorem MeasureTheory.Integrable.ofReal

added theorem MeasureTheory.Integrable.of_measure_le_smul

added theorem MeasureTheory.Integrable.pos_part

added theorem MeasureTheory.Integrable.prod_mk

added theorem MeasureTheory.Integrable.re

added theorem MeasureTheory.Integrable.re_im_iff

added theorem MeasureTheory.Integrable.real_toNNReal

added theorem MeasureTheory.Integrable.right_of_add_measure

added theorem MeasureTheory.Integrable.smul

added theorem MeasureTheory.Integrable.smul_const

added theorem MeasureTheory.Integrable.smul_essSup

added theorem MeasureTheory.Integrable.smul_measure

added theorem MeasureTheory.Integrable.smul_of_top_left

added theorem MeasureTheory.Integrable.smul_of_top_right

added theorem MeasureTheory.Integrable.sub

added theorem MeasureTheory.Integrable.sup

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.Integrable.to_average

added theorem MeasureTheory.Integrable.trim

added def MeasureTheory.Integrable

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

added theorem MeasureTheory.LipschitzWith.integrable_comp_iff_of_antilipschitz

added theorem MeasureTheory.MeasurePreserving.integrable_comp

added theorem MeasureTheory.MeasurePreserving.integrable_comp_emb

added theorem MeasureTheory.Memℒp.integrable

added theorem MeasureTheory.Memℒp.integrable_norm_rpow'

added theorem MeasureTheory.Memℒp.integrable_norm_rpow

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.coe_toNNReal_ae_eq

added theorem MeasureTheory.finiteMeasure_withDensity_ofReal

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_def

added theorem MeasureTheory.hasFiniteIntegral_iff_edist

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_of_lintegral_ne_top

added theorem MeasureTheory.hasFiniteIntegral_zero

added theorem MeasureTheory.hasFiniteIntegral_zero_measure

added theorem MeasureTheory.integrable_add_measure

added theorem MeasureTheory.integrable_average

added theorem MeasureTheory.integrable_congr'

added theorem MeasureTheory.integrable_congr

added theorem MeasureTheory.integrable_const

added theorem MeasureTheory.integrable_const_iff

added theorem MeasureTheory.integrable_const_mul_iff

added theorem MeasureTheory.integrable_def

added theorem MeasureTheory.integrable_finset_sum'

added theorem MeasureTheory.integrable_finset_sum

added theorem MeasureTheory.integrable_finset_sum_measure

added theorem MeasureTheory.integrable_inv_smul_measure

added theorem MeasureTheory.integrable_map_equiv

added theorem MeasureTheory.integrable_map_measure

added theorem MeasureTheory.integrable_mul_const_iff

added theorem MeasureTheory.integrable_neg_iff

added theorem MeasureTheory.integrable_norm_iff

added theorem MeasureTheory.integrable_of_forall_fin_meas_le'

added theorem MeasureTheory.integrable_of_forall_fin_meas_le

added theorem MeasureTheory.integrable_of_integrable_trim

added theorem MeasureTheory.integrable_of_norm_sub_le

added theorem MeasureTheory.integrable_smul_const

added theorem MeasureTheory.integrable_smul_iff

added theorem MeasureTheory.integrable_smul_measure

added theorem MeasureTheory.integrable_toReal_of_lintegral_ne_top

added theorem MeasureTheory.integrable_withDensity_iff

added theorem MeasureTheory.integrable_withDensity_iff_integrable_coe_smul

added theorem MeasureTheory.integrable_withDensity_iff_integrable_coe_smul₀

added theorem MeasureTheory.integrable_withDensity_iff_integrable_smul'

added theorem MeasureTheory.integrable_withDensity_iff_integrable_smul

added theorem MeasureTheory.integrable_withDensity_iff_integrable_smul₀

added theorem MeasureTheory.integrable_zero

added theorem MeasureTheory.integrable_zero_measure

added theorem MeasureTheory.lintegral_edist_lt_top

added theorem MeasureTheory.lintegral_edist_triangle

added theorem MeasureTheory.lintegral_nnnorm_add_left

added theorem MeasureTheory.lintegral_nnnorm_add_right

added theorem MeasureTheory.lintegral_nnnorm_eq_lintegral_edist

added theorem MeasureTheory.lintegral_nnnorm_neg

added theorem MeasureTheory.lintegral_nnnorm_zero

added theorem MeasureTheory.lintegral_norm_eq_lintegral_edist

added theorem MeasureTheory.mem_ℒ1_toReal_of_lintegral_ne_top

added theorem MeasureTheory.memℒ1_smul_of_L1_withDensity

added theorem MeasureTheory.memℒp_one_iff_integrable

added theorem MeasureTheory.ofReal_toReal_ae_eq

added theorem MeasureTheory.tendsto_lintegral_norm_of_dominated_convergence

added theorem MeasureTheory.withDensitySMulLI_apply

Modified Mathlib/MeasureTheory/Function/LpSeminorm.lean