Commit 2023-05-29 08:45 041f3da4

View on Github →

feat: port MeasureTheory.Function.LpSpace (#4341)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/LpSpace.lean

added theorem BoundedContinuousFunction.Lp_nnnorm_le

added theorem BoundedContinuousFunction.Lp_norm_le

added theorem BoundedContinuousFunction.coeFn_toLp

added theorem BoundedContinuousFunction.mem_Lp

added theorem BoundedContinuousFunction.range_toLp

added theorem BoundedContinuousFunction.range_toLpHom

added def BoundedContinuousFunction.toLp

added def BoundedContinuousFunction.toLpHom

added theorem BoundedContinuousFunction.toLp_inj

added theorem BoundedContinuousFunction.toLp_injective

added theorem BoundedContinuousFunction.toLp_norm_le

added theorem ContinuousLinearMap.add_compLp

added theorem ContinuousLinearMap.add_compLpL

added theorem ContinuousLinearMap.coeFn_compLp'

added theorem ContinuousLinearMap.coeFn_compLp

added theorem ContinuousLinearMap.coeFn_compLpL

added def ContinuousLinearMap.compLp

added def ContinuousLinearMap.compLpL

added def ContinuousLinearMap.compLpₗ

added theorem ContinuousLinearMap.comp_memℒp'

added theorem ContinuousLinearMap.comp_memℒp

added theorem ContinuousLinearMap.norm_compLpL_le

added theorem ContinuousLinearMap.norm_compLp_le

added theorem ContinuousLinearMap.smul_compLp

added theorem ContinuousLinearMap.smul_compLpL

added theorem ContinuousMap.coeFn_toLp

added theorem ContinuousMap.coe_toLp

added theorem ContinuousMap.hasSum_of_hasSum_Lp

added theorem ContinuousMap.range_toLp

added def ContinuousMap.toLp

added theorem ContinuousMap.toLp_comp_toContinuousMap

added theorem ContinuousMap.toLp_def

added theorem ContinuousMap.toLp_inj

added theorem ContinuousMap.toLp_injective

added theorem ContinuousMap.toLp_norm_eq_toLp_norm_coe

added theorem ContinuousMap.toLp_norm_le

added theorem LipschitzWith.coeFn_compLp

added def LipschitzWith.compLp

added theorem LipschitzWith.compLp_zero

added theorem LipschitzWith.comp_memℒp

added theorem LipschitzWith.continuous_compLp

added theorem LipschitzWith.lipschitzWith_compLp

added theorem LipschitzWith.memℒp_comp_iff_of_antilipschitz

added theorem LipschitzWith.norm_compLp_le

added theorem LipschitzWith.norm_compLp_sub_le

added def MeasureTheory.Lp.LpSubmodule

added theorem MeasureTheory.Lp.ae_tendsto_of_cauchy_snorm'

added theorem MeasureTheory.Lp.ae_tendsto_of_cauchy_snorm

added def MeasureTheory.Lp.boundedContinuousFunction

added theorem MeasureTheory.Lp.cauchySeq_Lp_iff_cauchySeq_ℒp

added theorem MeasureTheory.Lp.cauchy_complete_ℒp

added theorem MeasureTheory.Lp.cauchy_tendsto_of_tendsto

added theorem MeasureTheory.Lp.coeFn_add

added theorem MeasureTheory.Lp.coeFn_mk

added theorem MeasureTheory.Lp.coeFn_neg

added theorem MeasureTheory.Lp.coeFn_negPart

added theorem MeasureTheory.Lp.coeFn_negPart_eq_max

added theorem MeasureTheory.Lp.coeFn_posPart

added theorem MeasureTheory.Lp.coeFn_smul

added theorem MeasureTheory.Lp.coeFn_sub

added theorem MeasureTheory.Lp.coeFn_zero

added theorem MeasureTheory.Lp.coe_LpSubmodule

added theorem MeasureTheory.Lp.coe_mk

added theorem MeasureTheory.Lp.coe_posPart

added theorem MeasureTheory.Lp.completeSpace_lp_of_cauchy_complete_ℒp

added theorem MeasureTheory.Lp.continuous_negPart

added theorem MeasureTheory.Lp.continuous_posPart

added theorem MeasureTheory.Lp.dist_def

added theorem MeasureTheory.Lp.edist_def

added theorem MeasureTheory.Lp.edist_toLp_toLp

added theorem MeasureTheory.Lp.edist_toLp_zero

added theorem MeasureTheory.Lp.eq_zero_iff_ae_eq_zero

added theorem MeasureTheory.Lp.ext

added theorem MeasureTheory.Lp.ext_iff

added theorem MeasureTheory.Lp.lipschitzWith_pos_part

added theorem MeasureTheory.Lp.meas_ge_le_mul_pow_norm

added theorem MeasureTheory.Lp.mem_Lp_const_smul

added theorem MeasureTheory.Lp.mem_Lp_iff_memℒp

added theorem MeasureTheory.Lp.mem_Lp_iff_snorm_lt_top

added theorem MeasureTheory.Lp.mem_Lp_of_ae_bound

added theorem MeasureTheory.Lp.mem_Lp_of_ae_le

added theorem MeasureTheory.Lp.mem_Lp_of_ae_le_mul

added theorem MeasureTheory.Lp.mem_Lp_of_ae_nnnorm_bound

added theorem MeasureTheory.Lp.mem_Lp_of_nnnorm_ae_le

added theorem MeasureTheory.Lp.mem_Lp_of_nnnorm_ae_le_mul

added theorem MeasureTheory.Lp.mem_boundedContinuousFunction_iff

added theorem MeasureTheory.Lp.mem_lp_const

added theorem MeasureTheory.Lp.memℒp_of_cauchy_tendsto

added theorem MeasureTheory.Lp.mul_meas_ge_le_pow_norm'

added theorem MeasureTheory.Lp.mul_meas_ge_le_pow_norm

added def MeasureTheory.Lp.negPart

added theorem MeasureTheory.Lp.nnnorm_def

added theorem MeasureTheory.Lp.nnnorm_eq_zero_iff

added theorem MeasureTheory.Lp.nnnorm_le_mul_nnnorm_of_ae_le_mul

added theorem MeasureTheory.Lp.nnnorm_le_of_ae_bound

added theorem MeasureTheory.Lp.nnnorm_neg

added theorem MeasureTheory.Lp.nnnorm_toLp

added theorem MeasureTheory.Lp.nnnorm_zero

added theorem MeasureTheory.Lp.norm_def

added theorem MeasureTheory.Lp.norm_eq_zero_iff

added theorem MeasureTheory.Lp.norm_le_mul_norm_of_ae_le_mul

added theorem MeasureTheory.Lp.norm_le_norm_of_ae_le

added theorem MeasureTheory.Lp.norm_le_of_ae_bound

added theorem MeasureTheory.Lp.norm_neg

added theorem MeasureTheory.Lp.norm_toLp

added theorem MeasureTheory.Lp.norm_zero

added def MeasureTheory.Lp.posPart

added theorem MeasureTheory.Lp.pow_mul_meas_ge_le_norm

added theorem MeasureTheory.Lp.snorm'_lim_eq_lintegral_liminf

added theorem MeasureTheory.Lp.snorm'_lim_le_liminf_snorm'

added theorem MeasureTheory.Lp.snorm_exponent_top_lim_eq_essSup_liminf

added theorem MeasureTheory.Lp.snorm_exponent_top_lim_le_liminf_snorm_exponent_top

added theorem MeasureTheory.Lp.snorm_lim_le_liminf_snorm

added theorem MeasureTheory.Lp.snorm_lt_top

added theorem MeasureTheory.Lp.snorm_ne_top

added theorem MeasureTheory.Lp.tendsto_Lp_iff_tendsto_ℒp''

added theorem MeasureTheory.Lp.tendsto_Lp_iff_tendsto_ℒp'

added theorem MeasureTheory.Lp.tendsto_Lp_iff_tendsto_ℒp

added theorem MeasureTheory.Lp.tendsto_Lp_of_tendsto_ℒp

added theorem MeasureTheory.Lp.toLp_coeFn

added def MeasureTheory.Lp

added theorem MeasureTheory.Memℒp.coeFn_toLp

added theorem MeasureTheory.Memℒp.indicator

added theorem MeasureTheory.Memℒp.neg_part

added theorem MeasureTheory.Memℒp.norm_rpow

added theorem MeasureTheory.Memℒp.norm_rpow_div

added theorem MeasureTheory.Memℒp.ofReal

added theorem MeasureTheory.Memℒp.of_comp_antilipschitzWith

added theorem MeasureTheory.Memℒp.pos_part

added theorem MeasureTheory.Memℒp.snorm_mk_lt_top

added def MeasureTheory.Memℒp.toLp

added theorem MeasureTheory.Memℒp.toLp_add

added theorem MeasureTheory.Memℒp.toLp_congr

added theorem MeasureTheory.Memℒp.toLp_const_smul

added theorem MeasureTheory.Memℒp.toLp_eq_toLp_iff

added theorem MeasureTheory.Memℒp.toLp_neg

added theorem MeasureTheory.Memℒp.toLp_sub

added theorem MeasureTheory.Memℒp.toLp_zero

added theorem MeasureTheory.exists_snorm_indicator_le

added def MeasureTheory.indicatorConstLp

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_eq_toSpanSingleton_compLp

added theorem MeasureTheory.indicatorConst_empty

added theorem MeasureTheory.memℒp_add_of_disjoint

added theorem MeasureTheory.memℒp_indicator_const

added theorem MeasureTheory.memℒp_indicator_iff_restrict

added theorem MeasureTheory.memℒp_norm_rpow_iff

added theorem MeasureTheory.memℒp_re_im_iff

added theorem MeasureTheory.norm_indicatorConstLp'

added theorem MeasureTheory.norm_indicatorConstLp

added theorem MeasureTheory.norm_indicatorConstLp_top

added theorem MeasureTheory.snormEssSup_indicator_const_eq

added theorem MeasureTheory.snormEssSup_indicator_const_le

added theorem MeasureTheory.snormEssSup_indicator_eq_snormEssSup_restrict

added theorem MeasureTheory.snormEssSup_indicator_le

added theorem MeasureTheory.snorm_aeeqFun

added theorem MeasureTheory.snorm_indicator_const'

added theorem MeasureTheory.snorm_indicator_const

added theorem MeasureTheory.snorm_indicator_const_le

added theorem MeasureTheory.snorm_indicator_eq_snorm_restrict

added theorem MeasureTheory.snorm_indicator_le