Commit 2024-02-06 02:47 e415c3ba

View on Github →

chore(LpSeminorm): further split the file (#10207)

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/MeasureTheory/Function/LpSeminorm.lean to Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

deleted def MeasureTheory.LpAddConst

deleted theorem MeasureTheory.LpAddConst_lt_top

deleted theorem MeasureTheory.LpAddConst_of_one_le

deleted theorem MeasureTheory.LpAddConst_zero

deleted theorem MeasureTheory.Memℒp.add

deleted theorem MeasureTheory.Memℒp.memℒp_of_exponent_le

deleted theorem MeasureTheory.Memℒp.smul

deleted theorem MeasureTheory.Memℒp.smul_of_top_left

deleted theorem MeasureTheory.Memℒp.smul_of_top_right

deleted theorem MeasureTheory.Memℒp.sub

deleted theorem MeasureTheory.exists_Lp_half

deleted theorem MeasureTheory.meas_ge_le_mul_pow_snorm

deleted theorem MeasureTheory.memℒp_finset_sum'

deleted theorem MeasureTheory.memℒp_finset_sum

deleted theorem MeasureTheory.mul_meas_ge_le_pow_snorm'

deleted theorem MeasureTheory.mul_meas_ge_le_pow_snorm

deleted theorem MeasureTheory.pow_mul_meas_ge_le_snorm

deleted theorem MeasureTheory.snorm'_add_le

deleted theorem MeasureTheory.snorm'_add_le_of_le_one

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'_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_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

deleted theorem MeasureTheory.snorm_sub_le'

deleted theorem MeasureTheory.snorm_sub_le

deleted theorem MeasureTheory.snorm_sum_le

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

added theorem MeasureTheory.meas_ge_le_mul_pow_snorm

added theorem MeasureTheory.mul_meas_ge_le_pow_snorm'

added theorem MeasureTheory.mul_meas_ge_le_pow_snorm

added theorem MeasureTheory.pow_mul_meas_ge_le_snorm

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

added theorem MeasureTheory.Memℒp.memℒp_of_exponent_le

added theorem MeasureTheory.Memℒp.smul

added theorem MeasureTheory.Memℒp.smul_of_top_left

added theorem MeasureTheory.Memℒp.smul_of_top_right

added theorem MeasureTheory.snorm'_le_snorm'_mul_rpow_measure_univ

added theorem MeasureTheory.snorm'_le_snorm'_mul_snorm'

added theorem MeasureTheory.snorm'_le_snorm'_of_exponent_le

added theorem MeasureTheory.snorm'_le_snormEssSup

added theorem MeasureTheory.snorm'_le_snormEssSup_mul_rpow_measure_univ

added theorem MeasureTheory.snorm'_lt_top_of_snorm'_lt_top_of_exponent_le

added theorem MeasureTheory.snorm'_smul_le_mul_snorm'

added theorem MeasureTheory.snorm_le_snorm_mul_rpow_measure_univ

added theorem MeasureTheory.snorm_le_snorm_mul_snorm'_of_norm

added theorem MeasureTheory.snorm_le_snorm_mul_snorm_of_nnnorm

added theorem MeasureTheory.snorm_le_snorm_mul_snorm_top

added theorem MeasureTheory.snorm_le_snorm_of_exponent_le

added theorem MeasureTheory.snorm_le_snorm_top_mul_snorm

added theorem MeasureTheory.snorm_smul_le_mul_snorm

added theorem MeasureTheory.snorm_smul_le_snorm_mul_snorm_top

added theorem MeasureTheory.snorm_smul_le_snorm_top_mul_snorm

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

added theorem MeasureTheory.LpAddConst_lt_top

added theorem MeasureTheory.LpAddConst_of_one_le

added theorem MeasureTheory.LpAddConst_zero

added theorem MeasureTheory.Memℒp.add

added theorem MeasureTheory.Memℒp.sub

added theorem MeasureTheory.exists_Lp_half

added theorem MeasureTheory.memℒp_finset_sum'

added theorem MeasureTheory.memℒp_finset_sum

added theorem MeasureTheory.snorm'_add_le

added theorem MeasureTheory.snorm'_add_le_of_le_one

added theorem MeasureTheory.snorm'_sum_le

added theorem MeasureTheory.snormEssSup_add_le

added theorem MeasureTheory.snorm_add_le'

added theorem MeasureTheory.snorm_add_le

added theorem MeasureTheory.snorm_add_lt_top

added theorem MeasureTheory.snorm_sub_le'

added theorem MeasureTheory.snorm_sub_le

added theorem MeasureTheory.snorm_sum_le

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

Modified Mathlib/MeasureTheory/Function/LpSpace.lean