Theorems · Theorem · measure theory

ContinuousMap.toLp_denseRange

∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [inst_3 : BorelSpace α]
  (E : Type u_2) [inst_4 : NormedAddCommGroup E] (μ : MeasureTheory.Measure α) {p : ENNReal}
  [inst_5 : SecondCountableTopologyEither α E] [_i : Fact (1 ≤ p)] (𝕜 : Type u_3) [inst_6 : NormedRing 𝕜]
  [inst_7 : Module 𝕜 E] [inst_8 : IsBoundedSMul 𝕜 E] [NormedSpace ℝ E] [inst_10 : CompactSpace α] [μ.WeaklyRegular]
  [inst_12 : MeasureTheory.IsFiniteMeasure μ], p ≠ ⊤ → DenseRange ⇑(ContinuousMap.toLp p μ 𝕜)

Continuous functions are dense in MeasureTheory.Lp, 1 ≤ p < ∞. This theorem assumes that the domain is a compact space because otherwise ContinuousMap.toLp is undefined. Use BoundedContinuousFunction.toLp_denseRange if the domain is not a compact space.

Defined in

Mathlib.MeasureTheory.Function.ContinuousMapDense

Cited by

2 results in Mathlib

Foundations

Depth 236 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceNormalSpaceMeasurableSpaceBorelSpaceNormedAddCommGroupSecondCountableTopologyEitherFactNormedRingModuleIsBoundedSMulNormedSpaceCompactSpaceMeasureTheory.Measure.WeaklyRegularMeasureTheory.IsFiniteMeasure