Commit 2024-07-31 06:33 09e1ab33

View on Github →

chore(MeasureTheory): Rename snorm to eLpNorm (#15177)

eLpNorm for "extended Lp norm" is much more descriptive than snorm for "seminorm"
I need a NNReal-valued version of it, which I am planning to call nnLpNorm.

Estimated changes

Modified Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean

added def MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst

added theorem MeasureTheory.eLpNorm_le_eLpNorm_fderiv

added theorem MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq

added theorem MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq_inner

added theorem MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_le

added theorem MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one

deleted def MeasureTheory.snormLESNormFDerivOfEqInnerConst

deleted theorem MeasureTheory.snorm_le_snorm_fderiv

deleted theorem MeasureTheory.snorm_le_snorm_fderiv_of_eq

deleted theorem MeasureTheory.snorm_le_snorm_fderiv_of_eq_inner

deleted theorem MeasureTheory.snorm_le_snorm_fderiv_of_le

deleted theorem MeasureTheory.snorm_le_snorm_fderiv_one

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean

added theorem MeasureTheory.eLpNorm_condexpL2_le

deleted theorem MeasureTheory.snorm_condexpL2_le

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean

added theorem MeasureTheory.eLpNorm_one_condexp_le_eLpNorm

deleted theorem MeasureTheory.snorm_one_condexp_le_snorm

Modified Mathlib/MeasureTheory/Function/ContinuousMapDense.lean

added theorem MeasureTheory.Memℒp.exists_boundedContinuous_eLpNorm_sub_le

deleted theorem MeasureTheory.Memℒp.exists_boundedContinuous_snorm_sub_le

added theorem MeasureTheory.Memℒp.exists_hasCompactSupport_eLpNorm_sub_le

deleted theorem MeasureTheory.Memℒp.exists_hasCompactSupport_snorm_sub_le

added theorem MeasureTheory.exists_continuous_eLpNorm_sub_le_of_closed

deleted theorem MeasureTheory.exists_continuous_snorm_sub_le_of_closed

Modified Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

added theorem MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm

added theorem MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top

added theorem MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable

added theorem MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_top

deleted theorem MeasureTheory.tendstoInMeasure_of_tendsto_snorm

deleted theorem MeasureTheory.tendstoInMeasure_of_tendsto_snorm_of_ne_top

deleted theorem MeasureTheory.tendstoInMeasure_of_tendsto_snorm_of_stronglyMeasurable

deleted theorem MeasureTheory.tendstoInMeasure_of_tendsto_snorm_top

Modified Mathlib/MeasureTheory/Function/Intersectivity.lean

Modified Mathlib/MeasureTheory/Function/L1Space.lean

Modified Mathlib/MeasureTheory/Function/L2Space.lean

added theorem MeasureTheory.L2.eLpNorm_inner_lt_top

added theorem MeasureTheory.L2.eLpNorm_rpow_two_norm_lt_top

added theorem MeasureTheory.L2.integral_inner_eq_sq_eLpNorm

deleted theorem MeasureTheory.L2.integral_inner_eq_sq_snorm

deleted theorem MeasureTheory.L2.snorm_inner_lt_top

deleted theorem MeasureTheory.L2.snorm_rpow_two_norm_lt_top

Modified Mathlib/MeasureTheory/Function/LpOrder.lean

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

added theorem MeasurableEmbedding.eLpNormEssSup_map_measure

added theorem MeasurableEmbedding.eLpNorm_map_measure

deleted theorem MeasurableEmbedding.snormEssSup_map_measure

deleted theorem MeasurableEmbedding.snorm_map_measure

added theorem MeasureTheory.AEEqFun.eLpNorm_compMeasurePreserving

deleted theorem MeasureTheory.AEEqFun.snorm_compMeasurePreserving

added theorem MeasureTheory.Memℒp.eLpNorm_lt_top

added theorem MeasureTheory.Memℒp.eLpNorm_ne_top

added theorem MeasureTheory.Memℒp.exists_eLpNorm_indicator_compl_lt

deleted theorem MeasureTheory.Memℒp.exists_snorm_indicator_compl_lt

deleted theorem MeasureTheory.Memℒp.snorm_lt_top

deleted theorem MeasureTheory.Memℒp.snorm_ne_top

added theorem MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd

deleted theorem MeasureTheory.ae_bdd_liminf_atTop_of_snorm_bdd

added theorem MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd

deleted theorem MeasureTheory.ae_bdd_liminf_atTop_rpow_of_snorm_bdd

added theorem MeasureTheory.ae_eq_zero_of_eLpNorm'_eq_zero

deleted theorem MeasureTheory.ae_eq_zero_of_snorm'_eq_zero

added theorem MeasureTheory.ae_le_eLpNormEssSup

deleted theorem MeasureTheory.ae_le_snormEssSup

added theorem MeasureTheory.coe_nnnorm_ae_le_eLpNormEssSup

deleted theorem MeasureTheory.coe_nnnorm_ae_le_snormEssSup

added def MeasureTheory.eLpNorm'

added theorem MeasureTheory.eLpNorm'_congr_ae

added theorem MeasureTheory.eLpNorm'_congr_nnnorm_ae

added theorem MeasureTheory.eLpNorm'_congr_norm_ae

added theorem MeasureTheory.eLpNorm'_const'

added theorem MeasureTheory.eLpNorm'_const

added theorem MeasureTheory.eLpNorm'_const_of_isProbabilityMeasure

added theorem MeasureTheory.eLpNorm'_const_smul

added theorem MeasureTheory.eLpNorm'_const_smul_le

added theorem MeasureTheory.eLpNorm'_eq_zero_iff

added theorem MeasureTheory.eLpNorm'_eq_zero_of_ae_zero'

added theorem MeasureTheory.eLpNorm'_eq_zero_of_ae_zero

added theorem MeasureTheory.eLpNorm'_exponent_zero

added theorem MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul

added theorem MeasureTheory.eLpNorm'_measure_zero_of_exponent_zero

added theorem MeasureTheory.eLpNorm'_measure_zero_of_neg

added theorem MeasureTheory.eLpNorm'_measure_zero_of_pos

added theorem MeasureTheory.eLpNorm'_mono_ae

added theorem MeasureTheory.eLpNorm'_mono_measure

added theorem MeasureTheory.eLpNorm'_mono_nnnorm_ae

added theorem MeasureTheory.eLpNorm'_neg

added theorem MeasureTheory.eLpNorm'_norm

added theorem MeasureTheory.eLpNorm'_norm_rpow

added theorem MeasureTheory.eLpNorm'_smul_measure

added theorem MeasureTheory.eLpNorm'_zero'

added theorem MeasureTheory.eLpNorm'_zero

added def MeasureTheory.eLpNorm

added def MeasureTheory.eLpNormEssSup

added theorem MeasureTheory.eLpNormEssSup_congr_ae

added theorem MeasureTheory.eLpNormEssSup_const

added theorem MeasureTheory.eLpNormEssSup_const_smul

added theorem MeasureTheory.eLpNormEssSup_const_smul_le

added theorem MeasureTheory.eLpNormEssSup_eq_zero_iff

added theorem MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul

added theorem MeasureTheory.eLpNormEssSup_le_of_ae_bound

added theorem MeasureTheory.eLpNormEssSup_le_of_ae_nnnorm_bound

added theorem MeasureTheory.eLpNormEssSup_lt_top_of_ae_bound

added theorem MeasureTheory.eLpNormEssSup_lt_top_of_ae_nnnorm_bound

added theorem MeasureTheory.eLpNormEssSup_map_measure

added theorem MeasureTheory.eLpNormEssSup_measure_zero

added theorem MeasureTheory.eLpNormEssSup_mono_measure

added theorem MeasureTheory.eLpNormEssSup_mono_nnnorm_ae

added theorem MeasureTheory.eLpNormEssSup_piecewise

added theorem MeasureTheory.eLpNormEssSup_smul_measure

added theorem MeasureTheory.eLpNormEssSup_zero

added theorem MeasureTheory.eLpNorm_comp_measurePreserving

added theorem MeasureTheory.eLpNorm_congr_ae

added theorem MeasureTheory.eLpNorm_congr_nnnorm_ae

added theorem MeasureTheory.eLpNorm_congr_norm_ae

added theorem MeasureTheory.eLpNorm_const'

added theorem MeasureTheory.eLpNorm_const

added theorem MeasureTheory.eLpNorm_const_lt_top_iff

added theorem MeasureTheory.eLpNorm_const_smul

added theorem MeasureTheory.eLpNorm_const_smul_le

added theorem MeasureTheory.eLpNorm_eq_eLpNorm'

added theorem MeasureTheory.eLpNorm_eq_lintegral_rpow_nnnorm

added theorem MeasureTheory.eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg

added theorem MeasureTheory.eLpNorm_eq_zero_iff

added theorem MeasureTheory.eLpNorm_exponent_top

added theorem MeasureTheory.eLpNorm_exponent_zero

added theorem MeasureTheory.eLpNorm_indicator_eq_restrict

added theorem MeasureTheory.eLpNorm_indicator_sub_indicator

added theorem MeasureTheory.eLpNorm_le_add_measure_left

added theorem MeasureTheory.eLpNorm_le_add_measure_right

added theorem MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul

added theorem MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul

added theorem MeasureTheory.eLpNorm_le_of_ae_bound

added theorem MeasureTheory.eLpNorm_le_of_ae_nnnorm_bound

added theorem MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top

added theorem MeasureTheory.eLpNorm_map_measure

added theorem MeasureTheory.eLpNorm_measure_zero

added theorem MeasureTheory.eLpNorm_mono

added theorem MeasureTheory.eLpNorm_mono_ae

added theorem MeasureTheory.eLpNorm_mono_ae_real

added theorem MeasureTheory.eLpNorm_mono_measure

added theorem MeasureTheory.eLpNorm_mono_nnnorm

added theorem MeasureTheory.eLpNorm_mono_nnnorm_ae

added theorem MeasureTheory.eLpNorm_mono_real

added theorem MeasureTheory.eLpNorm_neg

added theorem MeasureTheory.eLpNorm_nnreal_eq_eLpNorm'

added theorem MeasureTheory.eLpNorm_nnreal_eq_lintegral

added theorem MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral

added theorem MeasureTheory.eLpNorm_norm

added theorem MeasureTheory.eLpNorm_norm_rpow

added theorem MeasureTheory.eLpNorm_one_add_measure

added theorem MeasureTheory.eLpNorm_one_eq_lintegral_nnnorm

added theorem MeasureTheory.eLpNorm_one_smul_measure

added theorem MeasureTheory.eLpNorm_restrict_eq_of_support_subset

added theorem MeasureTheory.eLpNorm_restrict_le

added theorem MeasureTheory.eLpNorm_smul_measure_of_ne_top

added theorem MeasureTheory.eLpNorm_smul_measure_of_ne_zero

added theorem MeasureTheory.eLpNorm_top_piecewise

added theorem MeasureTheory.eLpNorm_zero'

added theorem MeasureTheory.eLpNorm_zero

added theorem MeasureTheory.le_eLpNorm_of_bddBelow

deleted theorem MeasureTheory.le_snorm_of_bddBelow

added theorem MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_eLpNorm'

deleted theorem MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_snorm'

added theorem MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_eLpNorm'_lt_top

added theorem MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_eLpNorm_lt_top

deleted theorem MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top

deleted theorem MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top

added theorem MeasureTheory.meas_eLpNormEssSup_lt

deleted theorem MeasureTheory.meas_snormEssSup_lt

deleted def MeasureTheory.snorm'

deleted theorem MeasureTheory.snorm'_congr_ae

deleted theorem MeasureTheory.snorm'_congr_nnnorm_ae

deleted theorem MeasureTheory.snorm'_congr_norm_ae

deleted theorem MeasureTheory.snorm'_const'

deleted theorem MeasureTheory.snorm'_const

deleted theorem MeasureTheory.snorm'_const_of_isProbabilityMeasure

deleted theorem MeasureTheory.snorm'_const_smul

deleted theorem MeasureTheory.snorm'_const_smul_le

deleted theorem MeasureTheory.snorm'_eq_zero_iff

deleted theorem MeasureTheory.snorm'_eq_zero_of_ae_zero'

deleted theorem MeasureTheory.snorm'_eq_zero_of_ae_zero

deleted theorem MeasureTheory.snorm'_exponent_zero

deleted theorem MeasureTheory.snorm'_le_nnreal_smul_snorm'_of_ae_le_mul

deleted theorem MeasureTheory.snorm'_measure_zero_of_exponent_zero

deleted theorem MeasureTheory.snorm'_measure_zero_of_neg

deleted theorem MeasureTheory.snorm'_measure_zero_of_pos

deleted theorem MeasureTheory.snorm'_mono_ae

deleted theorem MeasureTheory.snorm'_mono_measure

deleted theorem MeasureTheory.snorm'_mono_nnnorm_ae

deleted theorem MeasureTheory.snorm'_neg

deleted theorem MeasureTheory.snorm'_norm

deleted theorem MeasureTheory.snorm'_norm_rpow

deleted theorem MeasureTheory.snorm'_smul_measure

deleted theorem MeasureTheory.snorm'_zero'

deleted theorem MeasureTheory.snorm'_zero

deleted def MeasureTheory.snorm

deleted def MeasureTheory.snormEssSup

deleted theorem MeasureTheory.snormEssSup_congr_ae

deleted theorem MeasureTheory.snormEssSup_const

deleted theorem MeasureTheory.snormEssSup_const_smul

deleted theorem MeasureTheory.snormEssSup_const_smul_le

deleted theorem MeasureTheory.snormEssSup_eq_zero_iff

deleted theorem MeasureTheory.snormEssSup_le_nnreal_smul_snormEssSup_of_ae_le_mul

deleted theorem MeasureTheory.snormEssSup_le_of_ae_bound

deleted theorem MeasureTheory.snormEssSup_le_of_ae_nnnorm_bound

deleted theorem MeasureTheory.snormEssSup_lt_top_of_ae_bound

deleted theorem MeasureTheory.snormEssSup_lt_top_of_ae_nnnorm_bound

deleted theorem MeasureTheory.snormEssSup_map_measure

deleted theorem MeasureTheory.snormEssSup_measure_zero

deleted theorem MeasureTheory.snormEssSup_mono_measure

deleted theorem MeasureTheory.snormEssSup_mono_nnnorm_ae

deleted theorem MeasureTheory.snormEssSup_piecewise

deleted theorem MeasureTheory.snormEssSup_smul_measure

deleted theorem MeasureTheory.snormEssSup_zero

deleted theorem MeasureTheory.snorm_comp_measurePreserving

deleted theorem MeasureTheory.snorm_congr_ae

deleted theorem MeasureTheory.snorm_congr_nnnorm_ae

deleted theorem MeasureTheory.snorm_congr_norm_ae

deleted theorem MeasureTheory.snorm_const'

deleted theorem MeasureTheory.snorm_const

deleted theorem MeasureTheory.snorm_const_lt_top_iff

deleted theorem MeasureTheory.snorm_const_smul

deleted theorem MeasureTheory.snorm_const_smul_le

deleted theorem MeasureTheory.snorm_eq_lintegral_rpow_nnnorm

deleted theorem MeasureTheory.snorm_eq_snorm'

deleted theorem MeasureTheory.snorm_eq_zero_and_zero_of_ae_le_mul_neg

deleted theorem MeasureTheory.snorm_eq_zero_iff

deleted theorem MeasureTheory.snorm_exponent_top

deleted theorem MeasureTheory.snorm_exponent_zero

deleted theorem MeasureTheory.snorm_indicator_eq_restrict

deleted theorem MeasureTheory.snorm_indicator_sub_indicator

deleted theorem MeasureTheory.snorm_le_add_measure_left

deleted theorem MeasureTheory.snorm_le_add_measure_right

deleted theorem MeasureTheory.snorm_le_mul_snorm_of_ae_le_mul

deleted theorem MeasureTheory.snorm_le_nnreal_smul_snorm_of_ae_le_mul

deleted theorem MeasureTheory.snorm_le_of_ae_bound

deleted theorem MeasureTheory.snorm_le_of_ae_nnnorm_bound

deleted theorem MeasureTheory.snorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top

deleted theorem MeasureTheory.snorm_map_measure

deleted theorem MeasureTheory.snorm_measure_zero

deleted theorem MeasureTheory.snorm_mono

deleted theorem MeasureTheory.snorm_mono_ae

deleted theorem MeasureTheory.snorm_mono_ae_real

deleted theorem MeasureTheory.snorm_mono_measure

deleted theorem MeasureTheory.snorm_mono_nnnorm

deleted theorem MeasureTheory.snorm_mono_nnnorm_ae

deleted theorem MeasureTheory.snorm_mono_real

deleted theorem MeasureTheory.snorm_neg

deleted theorem MeasureTheory.snorm_nnreal_eq_lintegral

deleted theorem MeasureTheory.snorm_nnreal_eq_snorm'

deleted theorem MeasureTheory.snorm_nnreal_pow_eq_lintegral

deleted theorem MeasureTheory.snorm_norm

deleted theorem MeasureTheory.snorm_norm_rpow

deleted theorem MeasureTheory.snorm_one_add_measure

deleted theorem MeasureTheory.snorm_one_eq_lintegral_nnnorm

deleted theorem MeasureTheory.snorm_one_smul_measure

deleted theorem MeasureTheory.snorm_restrict_eq_of_support_subset

deleted theorem MeasureTheory.snorm_restrict_le

deleted theorem MeasureTheory.snorm_smul_measure_of_ne_top

deleted theorem MeasureTheory.snorm_smul_measure_of_ne_zero

deleted theorem MeasureTheory.snorm_top_piecewise

deleted theorem MeasureTheory.snorm_zero'

deleted theorem MeasureTheory.snorm_zero

Modified Mathlib/MeasureTheory/Function/LpSeminorm/ChebyshevMarkov.lean

added theorem MeasureTheory.meas_ge_le_mul_pow_eLpNorm

deleted theorem MeasureTheory.meas_ge_le_mul_pow_snorm

added theorem MeasureTheory.mul_meas_ge_le_pow_eLpNorm'

added theorem MeasureTheory.mul_meas_ge_le_pow_eLpNorm

deleted theorem MeasureTheory.mul_meas_ge_le_pow_snorm'

deleted theorem MeasureTheory.mul_meas_ge_le_pow_snorm

added theorem MeasureTheory.pow_mul_meas_ge_le_eLpNorm

deleted theorem MeasureTheory.pow_mul_meas_ge_le_snorm

Modified Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean

added theorem MeasureTheory.eLpNorm'_le_eLpNorm'_mul_eLpNorm'

added theorem MeasureTheory.eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ

added theorem MeasureTheory.eLpNorm'_le_eLpNorm'_of_exponent_le

added theorem MeasureTheory.eLpNorm'_le_eLpNormEssSup

added theorem MeasureTheory.eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ

added theorem MeasureTheory.eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le

added theorem MeasureTheory.eLpNorm'_smul_le_mul_eLpNorm'

added theorem MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm

added theorem MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm

added theorem MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_top

added theorem MeasureTheory.eLpNorm_le_eLpNorm_mul_rpow_measure_univ

added theorem MeasureTheory.eLpNorm_le_eLpNorm_of_exponent_le

added theorem MeasureTheory.eLpNorm_le_eLpNorm_top_mul_eLpNorm

added theorem MeasureTheory.eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top

added theorem MeasureTheory.eLpNorm_smul_le_eLpNorm_top_mul_eLpNorm

added theorem MeasureTheory.eLpNorm_smul_le_mul_eLpNorm

deleted theorem MeasureTheory.snorm'_le_snorm'_mul_rpow_measure_univ

deleted theorem MeasureTheory.snorm'_le_snorm'_mul_snorm'

deleted theorem MeasureTheory.snorm'_le_snorm'_of_exponent_le

deleted theorem MeasureTheory.snorm'_le_snormEssSup

deleted theorem MeasureTheory.snorm'_le_snormEssSup_mul_rpow_measure_univ

deleted theorem MeasureTheory.snorm'_lt_top_of_snorm'_lt_top_of_exponent_le

deleted theorem MeasureTheory.snorm'_smul_le_mul_snorm'

deleted theorem MeasureTheory.snorm_le_snorm_mul_rpow_measure_univ

deleted theorem MeasureTheory.snorm_le_snorm_mul_snorm'_of_norm

deleted theorem MeasureTheory.snorm_le_snorm_mul_snorm_of_nnnorm

deleted theorem MeasureTheory.snorm_le_snorm_mul_snorm_top

deleted theorem MeasureTheory.snorm_le_snorm_of_exponent_le

deleted theorem MeasureTheory.snorm_le_snorm_top_mul_snorm

deleted theorem MeasureTheory.snorm_smul_le_mul_snorm

deleted theorem MeasureTheory.snorm_smul_le_snorm_mul_snorm_top

deleted theorem MeasureTheory.snorm_smul_le_snorm_top_mul_snorm

Modified Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean

added theorem MeasureTheory.eLpNorm'_add_le

added theorem MeasureTheory.eLpNorm'_add_le_of_le_one

added theorem MeasureTheory.eLpNorm'_sum_le

added theorem MeasureTheory.eLpNormEssSup_add_le

added theorem MeasureTheory.eLpNorm_add_le'

added theorem MeasureTheory.eLpNorm_add_le

added theorem MeasureTheory.eLpNorm_add_lt_top

added theorem MeasureTheory.eLpNorm_sub_le'

added theorem MeasureTheory.eLpNorm_sub_le

added theorem MeasureTheory.eLpNorm_sum_le

deleted theorem MeasureTheory.snorm'_add_le

deleted theorem MeasureTheory.snorm'_add_le_of_le_one

deleted theorem MeasureTheory.snorm'_sum_le

deleted theorem MeasureTheory.snormEssSup_add_le

deleted theorem MeasureTheory.snorm_add_le'

deleted theorem MeasureTheory.snorm_add_le

deleted theorem MeasureTheory.snorm_add_lt_top

deleted theorem MeasureTheory.snorm_sub_le'

deleted theorem MeasureTheory.snorm_sub_le

deleted theorem MeasureTheory.snorm_sum_le

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Trim.lean

added theorem MeasureTheory.eLpNorm'_trim

added theorem MeasureTheory.eLpNormEssSup_trim

added theorem MeasureTheory.eLpNorm_trim

added theorem MeasureTheory.eLpNorm_trim_ae

deleted theorem MeasureTheory.snorm'_trim

deleted theorem MeasureTheory.snormEssSup_trim

deleted theorem MeasureTheory.snorm_trim

deleted theorem MeasureTheory.snorm_trim_ae

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

added theorem MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm'

added theorem MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm

deleted theorem MeasureTheory.Lp.ae_tendsto_of_cauchy_snorm'

deleted theorem MeasureTheory.Lp.ae_tendsto_of_cauchy_snorm

modified theorem MeasureTheory.Lp.coeFn_mk

modified theorem MeasureTheory.Lp.coe_mk

modified theorem MeasureTheory.Lp.coe_nnnorm_toLp

modified theorem MeasureTheory.Lp.dist_def

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

added theorem MeasureTheory.Lp.eLpNorm_ne_top

modified theorem MeasureTheory.Lp.edist_def

modified theorem MeasureTheory.Lp.edist_toLp_zero

added theorem MeasureTheory.Lp.mem_Lp_iff_eLpNorm_lt_top

deleted theorem MeasureTheory.Lp.mem_Lp_iff_snorm_lt_top

modified theorem MeasureTheory.Lp.nnnorm_coe_ennreal

modified theorem MeasureTheory.Lp.nnnorm_def

modified theorem MeasureTheory.Lp.norm_def

modified theorem MeasureTheory.Lp.norm_toLp

deleted theorem MeasureTheory.Lp.snorm'_lim_eq_lintegral_liminf

deleted theorem MeasureTheory.Lp.snorm'_lim_le_liminf_snorm'

deleted theorem MeasureTheory.Lp.snorm_exponent_top_lim_eq_essSup_liminf

deleted theorem MeasureTheory.Lp.snorm_exponent_top_lim_le_liminf_snorm_exponent_top

deleted theorem MeasureTheory.Lp.snorm_lim_le_liminf_snorm

deleted theorem MeasureTheory.Lp.snorm_lt_top

deleted theorem MeasureTheory.Lp.snorm_ne_top

added theorem MeasureTheory.Memℒp.eLpNorm_mk_lt_top

deleted theorem MeasureTheory.Memℒp.snorm_mk_lt_top

added theorem MeasureTheory.eLpNormEssSup_indicator_const_eq

added theorem MeasureTheory.eLpNormEssSup_indicator_const_le

added theorem MeasureTheory.eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict

added theorem MeasureTheory.eLpNormEssSup_indicator_le

added theorem MeasureTheory.eLpNorm_aeeqFun

added theorem MeasureTheory.eLpNorm_indicator_const'

added theorem MeasureTheory.eLpNorm_indicator_const

added theorem MeasureTheory.eLpNorm_indicator_const_le

added theorem MeasureTheory.eLpNorm_indicator_const₀

added theorem MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict

added theorem MeasureTheory.eLpNorm_indicator_le

added theorem MeasureTheory.exists_eLpNorm_indicator_le

deleted theorem MeasureTheory.exists_snorm_indicator_le

deleted theorem MeasureTheory.snormEssSup_indicator_const_eq

deleted theorem MeasureTheory.snormEssSup_indicator_const_le

deleted theorem MeasureTheory.snormEssSup_indicator_eq_snormEssSup_restrict

deleted theorem MeasureTheory.snormEssSup_indicator_le

deleted theorem MeasureTheory.snorm_aeeqFun

deleted theorem MeasureTheory.snorm_indicator_const'

deleted theorem MeasureTheory.snorm_indicator_const

deleted theorem MeasureTheory.snorm_indicator_const_le

deleted theorem MeasureTheory.snorm_indicator_const₀

deleted theorem MeasureTheory.snorm_indicator_eq_snorm_restrict

deleted theorem MeasureTheory.snorm_indicator_le

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

added theorem MeasureTheory.Memℒp.exists_simpleFunc_eLpNorm_sub_lt

deleted theorem MeasureTheory.Memℒp.exists_simpleFunc_snorm_sub_lt

added theorem MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_eLpNorm

deleted theorem MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_snorm

added theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_eLpNorm

deleted theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_snorm

Modified Mathlib/MeasureTheory/Function/UnifTight.lean

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean

added theorem MeasureTheory.Memℒp.eLpNormEssSup_indicator_norm_ge_eq_zero

added theorem MeasureTheory.Memℒp.eLpNorm_indicator_le'

added theorem MeasureTheory.Memℒp.eLpNorm_indicator_le

added theorem MeasureTheory.Memℒp.eLpNorm_indicator_le_of_meas

added theorem MeasureTheory.Memℒp.eLpNorm_indicator_norm_ge_le

added theorem MeasureTheory.Memℒp.eLpNorm_indicator_norm_ge_pos_le

deleted theorem MeasureTheory.Memℒp.snormEssSup_indicator_norm_ge_eq_zero

deleted theorem MeasureTheory.Memℒp.snorm_indicator_le'

deleted theorem MeasureTheory.Memℒp.snorm_indicator_le

deleted theorem MeasureTheory.Memℒp.snorm_indicator_le_of_meas

deleted theorem MeasureTheory.Memℒp.snorm_indicator_norm_ge_le

deleted theorem MeasureTheory.Memℒp.snorm_indicator_norm_ge_pos_le

added theorem MeasureTheory.eLpNorm_indicator_le_of_bound

added theorem MeasureTheory.eLpNorm_sub_le_of_dist_bdd

deleted theorem MeasureTheory.snorm_indicator_le_of_bound

deleted theorem MeasureTheory.snorm_sub_le_of_dist_bdd

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

added theorem MeasureTheory.Memℒp.eLpNorm_eq_integral_rpow_norm

deleted theorem MeasureTheory.Memℒp.snorm_eq_integral_rpow_norm

added theorem MeasureTheory.eLpNorm_one_le_of_le'

added theorem MeasureTheory.eLpNorm_one_le_of_le

deleted theorem MeasureTheory.snorm_one_le_of_le'

deleted theorem MeasureTheory.snorm_one_le_of_le

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/MeasureTheory/Integral/MeanInequalities.lean

added theorem ENNReal.fun_eq_funMulInvSnorm_mul_eLpNorm

deleted theorem ENNReal.fun_eq_funMulInvSnorm_mul_snorm

added theorem ENNReal.lintegral_rpow_add_le_add_eLpNorm_mul_lintegral_rpow_add

deleted theorem ENNReal.lintegral_rpow_add_le_add_snorm_mul_lintegral_rpow_add

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

Modified Mathlib/Probability/IdentDistrib.lean

added theorem ProbabilityTheory.IdentDistrib.eLpNorm_eq

deleted theorem ProbabilityTheory.IdentDistrib.snorm_eq

Modified Mathlib/Probability/Kernel/Disintegration/CdfToKernel.lean

Modified Mathlib/Probability/Kernel/Disintegration/Density.lean

added theorem ProbabilityTheory.Kernel.eLpNorm_densityProcess_le

added theorem ProbabilityTheory.Kernel.eLpNorm_density_le

deleted theorem ProbabilityTheory.Kernel.snorm_densityProcess_le

deleted theorem ProbabilityTheory.Kernel.snorm_density_le

added theorem ProbabilityTheory.Kernel.tendsto_eLpNorm_one_densityProcess_limitProcess

added theorem ProbabilityTheory.Kernel.tendsto_eLpNorm_one_restrict_densityProcess_limitProcess

deleted theorem ProbabilityTheory.Kernel.tendsto_snorm_one_densityProcess_limitProcess

deleted theorem ProbabilityTheory.Kernel.tendsto_snorm_one_restrict_densityProcess_limitProcess

Modified Mathlib/Probability/Martingale/BorelCantelli.lean

added theorem MeasureTheory.Submartingale.stoppedValue_leastGE_eLpNorm_le'

added theorem MeasureTheory.Submartingale.stoppedValue_leastGE_eLpNorm_le

deleted theorem MeasureTheory.Submartingale.stoppedValue_leastGE_snorm_le'

deleted theorem MeasureTheory.Submartingale.stoppedValue_leastGE_snorm_le

Modified Mathlib/Probability/Martingale/Convergence.lean

added theorem MeasureTheory.Integrable.tendsto_eLpNorm_condexp

deleted theorem MeasureTheory.Integrable.tendsto_snorm_condexp

added theorem MeasureTheory.Martingale.eq_condexp_of_tendsto_eLpNorm

deleted theorem MeasureTheory.Martingale.eq_condexp_of_tendsto_snorm

added theorem MeasureTheory.Submartingale.tendsto_eLpNorm_one_limitProcess

deleted theorem MeasureTheory.Submartingale.tendsto_snorm_one_limitProcess

added theorem MeasureTheory.tendsto_eLpNorm_condexp

deleted theorem MeasureTheory.tendsto_snorm_condexp

Modified Mathlib/Probability/Process/Filtration.lean

added theorem MeasureTheory.Filtration.memℒp_limitProcess_of_eLpNorm_bdd

deleted theorem MeasureTheory.Filtration.memℒp_limitProcess_of_snorm_bdd

Modified Mathlib/Probability/StrongLaw.lean

Modified Mathlib/Probability/Variance.lean