OAI/Geometry/RCD/Sobolev/GammaL2Stability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.gammaL2_sub_norm_le line 15
2. theorem OAI.RegularPointCoordinates.gammaL2_tendsto line 35

   Source documentation

   Strong Sobolev convergence and a common gradient bound give strong L² convergence of the actual energy densities.

   theorem gammaL2_tendsto {u : ℕ → SobolevSpace μ hQ} {f : SobolevSpace μ hQ}
       (L : ℝ≥0)
       (hu : ∀ k, ∀ᵐ x ∂μ, SobolevSpace.minimalSlope μ hQ (u k) x ≤ L)
       (hf : ∀ᵐ x ∂μ, SobolevSpace.minimalSlope μ hQ f x ≤ L)
       (hconv : Tendsto u atTop (𝓝 f)) :
       Tendsto (fun k => (localGamma_memLp_of_bounded_gradient μ hQ (u k) (u k) L (hu k)).toLp
         (localGamma μ hQ (u k) (u k))) atTop
         (𝓝 ((localGamma_memLp_of_bounded_gradient μ hQ f f L hf).toLp (localGamma μ hQ f f))) := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.localGamma_memLp_of_bounded_gradient, OAI.RegularPointCoordinates.localGamma