Commit 2023-07-27 13:17 b9dadb41

View on Github →

feat: define MeasureTheory.Lp.const (#5236)

Estimated changes

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

added theorem MeasureTheory.Lp.coeFn_const

added theorem MeasureTheory.Lp.const_mem_Lp

added theorem MeasureTheory.Lp.const_smul_mem_Lp

added theorem MeasureTheory.Lp.const_val

deleted theorem MeasureTheory.Lp.mem_Lp_const_smul

deleted theorem MeasureTheory.Lp.mem_lp_const

added theorem MeasureTheory.Lp.norm_const'

added theorem MeasureTheory.Lp.norm_const

added theorem MeasureTheory.Lp.norm_constL_le

added theorem MeasureTheory.Lp.norm_const_le

added theorem MeasureTheory.Lp.norm_exponent_zero

added theorem MeasureTheory.Lp.norm_measure_zero

added theorem MeasureTheory.Memℒp.toLp_const

added theorem MeasureTheory.indicatorConstLp_univ

added theorem MeasureTheory.norm_indicatorConstLp_le