OAI/Geometry/RCD/Metric/BoundedCompactApproximation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.SobolevSpace.bounded_compact_L2_approximation line 18

   Source documentation

   Clip the compact recovery sequence to preserve the amplitude of the original bounded Sobolev function. L² convergence suffices after heat flow.

   theorem SobolevSpace.bounded_compact_L2_approximation (f : SobolevSpace μ hQ)
       (C : ℝ≥0) (hf : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ f x| ≤ C) (p : X) :
       ∃ (us : ℕ → Lp ℝ 2 μ) (gs : ℕ → X → ℝ),
         Tendsto us atTop (𝓝 (SobolevSpace.toLp μ hQ f)) ∧
         (∀ i, ∃ L : ℝ≥0, LipschitzWith L (gs i)) ∧
         (∀ i, HasCompactSupport (gs i)) ∧
         (∀ i, us i =ᵐ[μ] gs i) ∧ (∀ i x, |gs i x| ≤ C) := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp