Commit 2025-04-01 07:44 f926055d

View on Github →

chore: split MeasureTheory.Function.LpSpace.Basic (#23508) Split off

.Indicator for the indicator and constant functions as elements of Lp
.Complete for the completeness of Lp when 1 ≤ p

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

Modified Mathlib/MeasureTheory/Function/LpSpace/Basic.lean

deleted theorem Continuous.memLp_of_hasCompactSupport

deleted theorem HasCompactSupport.memLp_of_bound

deleted theorem MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm'

deleted theorem MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm

deleted theorem MeasureTheory.Lp.cauchySeq_Lp_iff_cauchySeq_eLpNorm

deleted theorem MeasureTheory.Lp.cauchy_complete_eLpNorm

deleted theorem MeasureTheory.Lp.cauchy_tendsto_of_tendsto

deleted theorem MeasureTheory.Lp.coeFn_const

deleted theorem MeasureTheory.Lp.completeSpace_lp_of_cauchy_complete_eLpNorm

deleted theorem MeasureTheory.Lp.const_val

deleted theorem MeasureTheory.Lp.eLpNorm'_lim_eq_lintegral_liminf

deleted theorem MeasureTheory.Lp.eLpNorm'_lim_le_liminf_eLpNorm'

deleted theorem MeasureTheory.Lp.eLpNorm_exponent_top_lim_eq_essSup_liminf

deleted theorem MeasureTheory.Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top

deleted theorem MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm

deleted theorem MeasureTheory.Lp.indicatorConstLp_compMeasurePreserving

deleted theorem MeasureTheory.Lp.memLp_of_cauchy_tendsto

deleted theorem MeasureTheory.Lp.norm_const'

deleted theorem MeasureTheory.Lp.norm_const

deleted theorem MeasureTheory.Lp.norm_constL_le

deleted theorem MeasureTheory.Lp.norm_const_le

deleted theorem MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm''

deleted theorem MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm'

deleted theorem MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm

deleted theorem MeasureTheory.Lp.tendsto_Lp_of_tendsto_eLpNorm

deleted theorem MeasureTheory.MemLp.toLp_const

deleted theorem MeasureTheory.continuous_indicatorConstLp_set

deleted theorem MeasureTheory.dist_indicatorConstLp_eq_norm

deleted theorem MeasureTheory.edist_indicatorConstLp_eq_enorm

deleted theorem MeasureTheory.enorm_indicatorConstLp_le

deleted theorem MeasureTheory.exists_eLpNorm_indicator_le

deleted def MeasureTheory.indicatorConstLp

deleted theorem MeasureTheory.indicatorConstLp_add

deleted theorem MeasureTheory.indicatorConstLp_coeFn

deleted theorem MeasureTheory.indicatorConstLp_coeFn_mem

deleted theorem MeasureTheory.indicatorConstLp_coeFn_nmem

deleted theorem MeasureTheory.indicatorConstLp_disjoint_union

deleted theorem MeasureTheory.indicatorConstLp_empty

deleted theorem MeasureTheory.indicatorConstLp_eq_toSpanSingleton_compLp

deleted theorem MeasureTheory.indicatorConstLp_inj

deleted theorem MeasureTheory.indicatorConstLp_sub

deleted theorem MeasureTheory.indicatorConstLp_univ

deleted theorem MeasureTheory.memLp_add_of_disjoint

deleted theorem MeasureTheory.nnnorm_indicatorConstLp_le

deleted theorem MeasureTheory.norm_indicatorConstLp'

deleted theorem MeasureTheory.norm_indicatorConstLp

deleted theorem MeasureTheory.norm_indicatorConstLp_le

deleted theorem MeasureTheory.norm_indicatorConstLp_top

deleted theorem MeasureTheory.tendsto_indicatorConstLp_set

Created Mathlib/MeasureTheory/Function/LpSpace/Complete.lean

added theorem MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm'

added theorem MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm

added theorem MeasureTheory.Lp.cauchySeq_Lp_iff_cauchySeq_eLpNorm

added theorem MeasureTheory.Lp.cauchy_complete_eLpNorm

added theorem MeasureTheory.Lp.cauchy_tendsto_of_tendsto

added theorem MeasureTheory.Lp.completeSpace_lp_of_cauchy_complete_eLpNorm

added theorem MeasureTheory.Lp.eLpNorm'_lim_eq_lintegral_liminf

added theorem MeasureTheory.Lp.eLpNorm'_lim_le_liminf_eLpNorm'

added theorem MeasureTheory.Lp.eLpNorm_exponent_top_lim_eq_essSup_liminf

added theorem MeasureTheory.Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top

added theorem MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm

added theorem MeasureTheory.Lp.memLp_of_cauchy_tendsto

added theorem MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm''

added theorem MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm'

added theorem MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm

added theorem MeasureTheory.Lp.tendsto_Lp_of_tendsto_eLpNorm

Modified Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean

Created Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean

added theorem Continuous.memLp_of_hasCompactSupport

added theorem HasCompactSupport.memLp_of_bound

added theorem MeasureTheory.Lp.coeFn_const

added theorem MeasureTheory.Lp.const_val

added theorem MeasureTheory.Lp.indicatorConstLp_compMeasurePreserving

added theorem MeasureTheory.Lp.norm_const'

added theorem MeasureTheory.Lp.norm_const

added theorem MeasureTheory.Lp.norm_constL_le

added theorem MeasureTheory.Lp.norm_const_le

added theorem MeasureTheory.MemLp.toLp_const

added theorem MeasureTheory.continuous_indicatorConstLp_set

added theorem MeasureTheory.dist_indicatorConstLp_eq_norm

added theorem MeasureTheory.edist_indicatorConstLp_eq_enorm

added theorem MeasureTheory.enorm_indicatorConstLp_le

added theorem MeasureTheory.exists_eLpNorm_indicator_le

added def MeasureTheory.indicatorConstLp

added theorem MeasureTheory.indicatorConstLp_add

added theorem MeasureTheory.indicatorConstLp_coeFn

added theorem MeasureTheory.indicatorConstLp_coeFn_mem

added theorem MeasureTheory.indicatorConstLp_coeFn_nmem

added theorem MeasureTheory.indicatorConstLp_disjoint_union

added theorem MeasureTheory.indicatorConstLp_empty

added theorem MeasureTheory.indicatorConstLp_eq_toSpanSingleton_compLp

added theorem MeasureTheory.indicatorConstLp_inj

added theorem MeasureTheory.indicatorConstLp_sub

added theorem MeasureTheory.indicatorConstLp_univ

added theorem MeasureTheory.memLp_add_of_disjoint

added theorem MeasureTheory.nnnorm_indicatorConstLp_le

added theorem MeasureTheory.norm_indicatorConstLp'

added theorem MeasureTheory.norm_indicatorConstLp

added theorem MeasureTheory.norm_indicatorConstLp_le

added theorem MeasureTheory.norm_indicatorConstLp_top

added theorem MeasureTheory.tendsto_indicatorConstLp_set

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean