OAI/Geometry/RCD/Metric/BoundedContinuousL2Approximation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact continuous approximation preserving a uniform amplitude

  1. theorem OAI.RegularPointCoordinates.exists_bounded_continuous_L2_approximation line 18

    Source documentation

    A bounded L² class has uniformly bounded compact continuous approximants.

    theorem exists_bounded_continuous_L2_approximation (f : Lp ℝ 2 μ) (C : ℝ≥0)
    (hf : ∀ᵐ x ∂μ, |f x| ≤ C) :
    ∃ F : ℕ → C_c(X, ℝ), (∀ i x, |F i x| ≤ C) ∧
      Tendsto (fun i => compactTestToL2 μ (F i)) atTop (𝓝 f) := by
…

    Mentions: OAI.RegularPointCoordinates.compactTestToL2