Commit 2023-05-28 20:07 54f2da2b

View on Github →

feat: port MeasureTheory.Function.LpSeminorm (#4445)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/LpSeminorm.lean

added theorem MeasurableEmbedding.memℒp_map_measure_iff

added theorem MeasurableEmbedding.snormEssSup_map_measure

added theorem MeasurableEmbedding.snorm_map_measure

added theorem MeasurableEquiv.memℒp_map_measure_iff

added def MeasureTheory.LpAddConst

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

added theorem MeasureTheory.Memℒp.aestronglyMeasurable

added theorem MeasureTheory.Memℒp.congr_norm

added theorem MeasureTheory.Memℒp.const_mul

added theorem MeasureTheory.Memℒp.const_smul

added theorem MeasureTheory.Memℒp.im

added theorem MeasureTheory.Memℒp.left_of_add_measure

added theorem MeasureTheory.Memℒp.memℒp_of_exponent_le

added theorem MeasureTheory.Memℒp.mono'

added theorem MeasureTheory.Memℒp.mono_measure

added theorem MeasureTheory.Memℒp.neg

added theorem MeasureTheory.Memℒp.norm

added theorem MeasureTheory.Memℒp.of_bound

added theorem MeasureTheory.Memℒp.of_le

added theorem MeasureTheory.Memℒp.of_le_mul

added theorem MeasureTheory.Memℒp.of_measure_le_smul

added theorem MeasureTheory.Memℒp.of_nnnorm_le_mul

added theorem MeasureTheory.Memℒp.re

added theorem MeasureTheory.Memℒp.restrict

added theorem MeasureTheory.Memℒp.right_of_add_measure

added theorem MeasureTheory.Memℒp.smul

added theorem MeasureTheory.Memℒp.smul_measure

added theorem MeasureTheory.Memℒp.smul_of_top_left

added theorem MeasureTheory.Memℒp.smul_of_top_right

added theorem MeasureTheory.Memℒp.snorm_lt_top

added theorem MeasureTheory.Memℒp.snorm_ne_top

added theorem MeasureTheory.Memℒp.sub

added def MeasureTheory.Memℒp

added theorem MeasureTheory.ae_bdd_liminf_atTop_of_snorm_bdd

added theorem MeasureTheory.ae_bdd_liminf_atTop_rpow_of_snorm_bdd

added theorem MeasureTheory.ae_eq_zero_of_snorm'_eq_zero

added theorem MeasureTheory.ae_le_snormEssSup

added theorem MeasureTheory.coe_nnnorm_ae_le_snormEssSup

added theorem MeasureTheory.essSup_trim

added theorem MeasureTheory.exists_Lp_half

added theorem MeasureTheory.limsup_trim

added theorem MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_snorm'

added theorem MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top

added theorem MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top

added theorem MeasureTheory.meas_ge_le_mul_pow_snorm

added theorem MeasureTheory.meas_snormEssSup_lt

added theorem MeasureTheory.memℒp_congr_ae

added theorem MeasureTheory.memℒp_congr_norm

added theorem MeasureTheory.memℒp_const

added theorem MeasureTheory.memℒp_const_iff

added theorem MeasureTheory.memℒp_def

added theorem MeasureTheory.memℒp_finset_sum'

added theorem MeasureTheory.memℒp_finset_sum

added theorem MeasureTheory.memℒp_map_measure_iff

added theorem MeasureTheory.memℒp_neg_iff

added theorem MeasureTheory.memℒp_norm_iff

added theorem MeasureTheory.memℒp_of_memℒp_trim

added theorem MeasureTheory.memℒp_top_const

added theorem MeasureTheory.memℒp_top_of_bound

added theorem MeasureTheory.memℒp_zero_iff_aestronglyMeasurable

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

added def MeasureTheory.snorm'

added theorem MeasureTheory.snorm'_add_le

added theorem MeasureTheory.snorm'_add_le_of_le_one

added theorem MeasureTheory.snorm'_congr_ae

added theorem MeasureTheory.snorm'_congr_nnnorm_ae

added theorem MeasureTheory.snorm'_congr_norm_ae

added theorem MeasureTheory.snorm'_const'

added theorem MeasureTheory.snorm'_const

added theorem MeasureTheory.snorm'_const_of_probabilityMeasure

added theorem MeasureTheory.snorm'_const_smul

added theorem MeasureTheory.snorm'_const_smul_le

added theorem MeasureTheory.snorm'_eq_zero_iff

added theorem MeasureTheory.snorm'_eq_zero_of_ae_zero'

added theorem MeasureTheory.snorm'_eq_zero_of_ae_zero

added theorem MeasureTheory.snorm'_exponent_zero

added theorem MeasureTheory.snorm'_le_nnreal_smul_snorm'_of_ae_le_mul

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

added theorem MeasureTheory.snorm'_measure_zero_of_neg

added theorem MeasureTheory.snorm'_measure_zero_of_pos

added theorem MeasureTheory.snorm'_mono_ae

added theorem MeasureTheory.snorm'_mono_measure

added theorem MeasureTheory.snorm'_mono_nnnorm_ae

added theorem MeasureTheory.snorm'_neg

added theorem MeasureTheory.snorm'_norm

added theorem MeasureTheory.snorm'_norm_rpow

added theorem MeasureTheory.snorm'_smul_le_mul_snorm'

added theorem MeasureTheory.snorm'_smul_measure

added theorem MeasureTheory.snorm'_sum_le

added theorem MeasureTheory.snorm'_trim

added theorem MeasureTheory.snorm'_zero'

added theorem MeasureTheory.snorm'_zero

added def MeasureTheory.snorm

added def MeasureTheory.snormEssSup

added theorem MeasureTheory.snormEssSup_add_le

added theorem MeasureTheory.snormEssSup_congr_ae

added theorem MeasureTheory.snormEssSup_const

added theorem MeasureTheory.snormEssSup_const_smul

added theorem MeasureTheory.snormEssSup_const_smul_le

added theorem MeasureTheory.snormEssSup_eq_zero_iff

added theorem MeasureTheory.snormEssSup_le_nnreal_smul_snormEssSup_of_ae_le_mul

added theorem MeasureTheory.snormEssSup_le_of_ae_bound

added theorem MeasureTheory.snormEssSup_le_of_ae_nnnorm_bound

added theorem MeasureTheory.snormEssSup_lt_top_of_ae_bound

added theorem MeasureTheory.snormEssSup_lt_top_of_ae_nnnorm_bound

added theorem MeasureTheory.snormEssSup_map_measure

added theorem MeasureTheory.snormEssSup_measure_zero

added theorem MeasureTheory.snormEssSup_mono_measure

added theorem MeasureTheory.snormEssSup_mono_nnnorm_ae

added theorem MeasureTheory.snormEssSup_smul_measure

added theorem MeasureTheory.snormEssSup_trim

added theorem MeasureTheory.snormEssSup_zero

added theorem MeasureTheory.snorm_add_le'

added theorem MeasureTheory.snorm_add_le

added theorem MeasureTheory.snorm_add_lt_top

added theorem MeasureTheory.snorm_congr_ae

added theorem MeasureTheory.snorm_congr_nnnorm_ae

added theorem MeasureTheory.snorm_congr_norm_ae

added theorem MeasureTheory.snorm_const'

added theorem MeasureTheory.snorm_const

added theorem MeasureTheory.snorm_const_lt_top_iff

added theorem MeasureTheory.snorm_const_smul

added theorem MeasureTheory.snorm_const_smul_le

added theorem MeasureTheory.snorm_eq_lintegral_rpow_nnnorm

added theorem MeasureTheory.snorm_eq_snorm'

added theorem MeasureTheory.snorm_eq_zero_and_zero_of_ae_le_mul_neg

added theorem MeasureTheory.snorm_eq_zero_iff

added theorem MeasureTheory.snorm_exponent_top

added theorem MeasureTheory.snorm_exponent_zero

added theorem MeasureTheory.snorm_indicator_ge_of_bdd_below

added theorem MeasureTheory.snorm_le_add_measure_left

added theorem MeasureTheory.snorm_le_add_measure_right

added theorem MeasureTheory.snorm_le_mul_snorm_of_ae_le_mul

added theorem MeasureTheory.snorm_le_nnreal_smul_snorm_of_ae_le_mul

added theorem MeasureTheory.snorm_le_of_ae_bound

added theorem MeasureTheory.snorm_le_of_ae_nnnorm_bound

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_lt_top_iff_lintegral_rpow_nnnorm_lt_top

added theorem MeasureTheory.snorm_map_measure

added theorem MeasureTheory.snorm_measure_zero

added theorem MeasureTheory.snorm_mono

added theorem MeasureTheory.snorm_mono_ae

added theorem MeasureTheory.snorm_mono_ae_real

added theorem MeasureTheory.snorm_mono_measure

added theorem MeasureTheory.snorm_mono_nnnorm

added theorem MeasureTheory.snorm_mono_nnnorm_ae

added theorem MeasureTheory.snorm_mono_real

added theorem MeasureTheory.snorm_neg

added theorem MeasureTheory.snorm_norm

added theorem MeasureTheory.snorm_norm_rpow

added theorem MeasureTheory.snorm_one_add_measure

added theorem MeasureTheory.snorm_one_eq_lintegral_nnnorm

added theorem MeasureTheory.snorm_one_smul_measure

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

added theorem MeasureTheory.snorm_smul_measure_of_ne_top

added theorem MeasureTheory.snorm_smul_measure_of_ne_zero

added theorem MeasureTheory.snorm_sub_le'

added theorem MeasureTheory.snorm_sub_le

added theorem MeasureTheory.snorm_sum_le

added theorem MeasureTheory.snorm_trim

added theorem MeasureTheory.snorm_trim_ae

added theorem MeasureTheory.snorm_zero'

added theorem MeasureTheory.snorm_zero

added theorem MeasureTheory.zero_mem_ℒp'

added theorem MeasureTheory.zero_memℒp