theorem
LpCompleteness.lp_banach_space
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{E : Type u_2}
[NormedAddCommGroup E]
[CompleteSpace E]
{p : ENNReal}
[hp : Fact (1 ≤ p)]
:
CompleteSpace ↥(MeasureTheory.Lp E p μ)
theorem
LpCompleteness.smooth_compactSupport_dense_Lp_Rn
(n : ℕ)
{p : ENNReal}
(hp_top : p ≠ ⊤)
[hp : Fact (1 ≤ p)]
:
Dense
{f : ↥(MeasureTheory.Lp ℂ p MeasureTheory.volume) | ∃ (g : EuclideanSpace ℝ (Fin n) → ℂ), ↑↑f =ᵐ[MeasureTheory.volume] g ∧ HasCompactSupport g ∧ ContDiff ℝ (↑⊤) g}