Commit 2023-06-02 11:07 a2ba3ef7

View on Github →

feat: port MeasureTheory.Function.SimpleFuncDenseLp (#4521)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

added theorem MeasureTheory.Integrable.induction

added theorem MeasureTheory.L1.SimpleFunc.toLp_one_eq_toL1

added theorem MeasureTheory.Lp.induction

added theorem MeasureTheory.Lp.simpleFunc.add_toSimpleFunc

added theorem MeasureTheory.Lp.simpleFunc.coeFn_le

added theorem MeasureTheory.Lp.simpleFunc.coeFn_nonneg

added theorem MeasureTheory.Lp.simpleFunc.coeFn_zero

added def MeasureTheory.Lp.simpleFunc.coeSimpleFuncNonnegToLpNonneg

added def MeasureTheory.Lp.simpleFunc.coeToLp

added theorem MeasureTheory.Lp.simpleFunc.coe_indicatorConst

added theorem MeasureTheory.Lp.simpleFunc.coe_smul

added theorem MeasureTheory.Lp.simpleFunc.denseRange_coeSimpleFuncNonnegToLpNonneg

added theorem MeasureTheory.Lp.simpleFunc.exists_simpleFunc_nonneg_ae_eq

added def MeasureTheory.Lp.simpleFunc.indicatorConst

added theorem MeasureTheory.Lp.simpleFunc.neg_toSimpleFunc

added theorem MeasureTheory.Lp.simpleFunc.norm_toSimpleFunc

added theorem MeasureTheory.Lp.simpleFunc.smul_toSimpleFunc

added theorem MeasureTheory.Lp.simpleFunc.sub_toSimpleFunc

added def MeasureTheory.Lp.simpleFunc.toLp

added theorem MeasureTheory.Lp.simpleFunc.toLp_add

added theorem MeasureTheory.Lp.simpleFunc.toLp_eq_mk

added theorem MeasureTheory.Lp.simpleFunc.toLp_eq_toLp

added theorem MeasureTheory.Lp.simpleFunc.toLp_neg

added theorem MeasureTheory.Lp.simpleFunc.toLp_smul

added theorem MeasureTheory.Lp.simpleFunc.toLp_sub

added theorem MeasureTheory.Lp.simpleFunc.toLp_toSimpleFunc

added theorem MeasureTheory.Lp.simpleFunc.toLp_zero

added def MeasureTheory.Lp.simpleFunc.toSimpleFunc

added theorem MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun

added theorem MeasureTheory.Lp.simpleFunc.toSimpleFunc_indicatorConst

added theorem MeasureTheory.Lp.simpleFunc.toSimpleFunc_toLp

added theorem MeasureTheory.Lp.simpleFunc.zero_toSimpleFunc

added def MeasureTheory.Lp.simpleFunc

added theorem MeasureTheory.Memℒp.exists_simpleFunc_snorm_sub_lt

added theorem MeasureTheory.Memℒp.induction

added theorem MeasureTheory.Memℒp.induction_dense

added theorem MeasureTheory.SimpleFunc.FinMeasSupp.integrable

added theorem MeasureTheory.SimpleFunc.exists_forall_norm_le

added theorem MeasureTheory.SimpleFunc.integrable_approxOn

added theorem MeasureTheory.SimpleFunc.integrable_approxOn_range

added theorem MeasureTheory.SimpleFunc.integrable_iff

added theorem MeasureTheory.SimpleFunc.integrable_iff_finMeasSupp

added theorem MeasureTheory.SimpleFunc.integrable_of_finiteMeasure

added theorem MeasureTheory.SimpleFunc.integrable_pair

added theorem MeasureTheory.SimpleFunc.measure_lt_top_of_memℒp_indicator

added theorem MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_integrable

added theorem MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_memℒp

added theorem MeasureTheory.SimpleFunc.measure_support_lt_top

added theorem MeasureTheory.SimpleFunc.measure_support_lt_top_of_integrable

added theorem MeasureTheory.SimpleFunc.measure_support_lt_top_of_memℒp

added theorem MeasureTheory.SimpleFunc.memℒp_approxOn

added theorem MeasureTheory.SimpleFunc.memℒp_approxOn_range

added theorem MeasureTheory.SimpleFunc.memℒp_iff

added theorem MeasureTheory.SimpleFunc.memℒp_iff_finMeasSupp

added theorem MeasureTheory.SimpleFunc.memℒp_iff_integrable

added theorem MeasureTheory.SimpleFunc.memℒp_of_finiteMeasure

added theorem MeasureTheory.SimpleFunc.memℒp_of_finite_measure_preimage

added theorem MeasureTheory.SimpleFunc.memℒp_top

added theorem MeasureTheory.SimpleFunc.memℒp_zero

added theorem MeasureTheory.SimpleFunc.nnnorm_approxOn_le

added theorem MeasureTheory.SimpleFunc.norm_approxOn_y₀_le

added theorem MeasureTheory.SimpleFunc.norm_approxOn_zero_le

added theorem MeasureTheory.SimpleFunc.tendsto_approxOn_L1_nnnorm

added theorem MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_snorm

added theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_nnnorm

added theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp

added theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_snorm