LocalPoissonRegularExtension.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Regular-core extensions retaining the local Poisson source

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_poisson_regular_extension line 18

Source documentation

The compact extension belongs to the actual regular core, and its L² Laplacian retains the original constant on the entire plateau.

theorem NoncollapsedRCD.local_poisson_regular_extension {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2≤n)
    (f : SobolevSpace (hausdorff n X) hX.quadratic) (c : ℝ)
    {p : X} {R b : ℝ} (hR : 0<R) (hRb : 2*R<b)
    (hf : IsConstantLaplacianOn (hausdorff n X) hX.quadratic (ball p b) f c)
    (L : ℝ≥0) (hL : ∀ᵐ x ∂(hausdorff n X).restrict (ball p b),
      localGamma (hausdorff n X) hX.quadratic f f x≤(L:ℝ)^2) :
    ∃ (F : compactLaplacianCore (hausdorff n X) hX.quadratic univ)
      (d : Lp ℝ 2 (hausdorff n X)),
      IsWeakLaplacian (hausdorff n X) hX.quadratic F.val d ∧
      SobolevSpace.toLp (hausdorff n X) hX.quadratic F.val
        =ᵐ[(hausdorff n X).restrict (ball p R)] SobolevSpace.toLp (hausdorff n X) hX.quadratic f ∧
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.compactLaplacianCore, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.SobolevSpace.toLp