Commit 2025-02-12 17:50 1c5e1606

View on Github →

chore(MeasureTheory/Function/LpSpace.lean): split out material on (bounded) continuous functions (#21783) and move LpSpace.lean to LpSpace/Basic.lean. Barely addresses a long file warning.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Function/ContinuousMapDense.lean

Modified Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

Modified Mathlib/MeasureTheory/Function/L2Space.lean

Modified Mathlib/MeasureTheory/Function/LpOrder.lean

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

deleted theorem BoundedContinuousFunction.Lp_nnnorm_le

deleted theorem BoundedContinuousFunction.Lp_norm_le

deleted theorem BoundedContinuousFunction.coeFn_toLp

deleted theorem BoundedContinuousFunction.mem_Lp

deleted theorem BoundedContinuousFunction.range_toLp

deleted theorem BoundedContinuousFunction.range_toLpHom

deleted def BoundedContinuousFunction.toLp

deleted def BoundedContinuousFunction.toLpHom

deleted theorem BoundedContinuousFunction.toLp_inj

deleted theorem BoundedContinuousFunction.toLp_injective

deleted theorem BoundedContinuousFunction.toLp_norm_le

deleted theorem ContinuousMap.coeFn_toLp

deleted theorem ContinuousMap.coe_toLp

deleted theorem ContinuousMap.hasSum_of_hasSum_Lp

deleted theorem ContinuousMap.range_toLp

deleted def ContinuousMap.toLp

deleted theorem ContinuousMap.toLp_comp_toContinuousMap

deleted theorem ContinuousMap.toLp_def

deleted theorem ContinuousMap.toLp_inj

deleted theorem ContinuousMap.toLp_injective

deleted theorem ContinuousMap.toLp_norm_eq_toLp_norm_coe

deleted theorem ContinuousMap.toLp_norm_le

deleted def MeasureTheory.Lp.boundedContinuousFunction

deleted theorem MeasureTheory.Lp.mem_boundedContinuousFunction_iff

Created Mathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.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 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 def MeasureTheory.Lp.boundedContinuousFunction

added theorem MeasureTheory.Lp.mem_boundedContinuousFunction_iff

Modified Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean