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}