`PhysFunctionalAnalysis.polynomial_dense_L2` : Dense {f : Lp ℝ 2 unitMeasure | ∃ P : Polynomial ℝ, f =ᵐ[unitMeasure] fun x => P.eval x}

Proved

PhysFunctionalAnalysis.polynomial_dense_L2

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from PhysFunctionalAnalysis.

PhysFunctionalAnalysis.polynomial_dense_L2 : Dense {f : Lp ℝ 2 unitMeasure | ∃ P : Polynomial ℝ, f =ᵐ[unitMeasure] fun x => P.eval x}

Formalization note: Lean 4 identifier PhysFunctionalAnalysis.polynomial_dense_L2.

Preamble

-- Generated from PhysFunctionalAnalysis.lean — theorem PhysFunctionalAnalysis.polynomial_dense_L2
import Mathlib
import Definitions.Def_PhysFunctionalAnalysis
import Definitions.Def_PhysMeasureBasis
import Definitions.Def_ChapterA4
open PhysMeasureBasis
open PhysFunctionalAnalysis


open MeasureTheory Set
open scoped ENNReal lp

noncomputable section


open PhysMeasureBasis

Formal statement

theorem PhysFunctionalAnalysis.polynomial_dense_L2 :
    Dense {f : Lp ℝ 2 unitMeasure | ∃ P : Polynomial ℝ,
           f =ᵐ[unitMeasure] fun x => P.eval x} := by sorry

View graph