DistanceLaplacianInput.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The exact distance-Laplacian input

Gigli, On the differential structure of metric measure spaces and applications, Mem. AMS 236 (2015), Corollary 5.15, equation (5.29), and Theorem 5.3, give the local distance eikonal identity and the positive Laplacian defect. The elementary hyperbolic comparison bounds the density by n + kappa R² on B_R when Ricci is bounded below by -kappa.

def OAI.RegularPointCoordinates.LocalSquaredDistanceInput line 23

theorem OAI.RegularPointCoordinates.positiveSquaredDistance_source line 43

Source documentation

Adding the cutoff constant leaves the source unchanged on the working ball, and compact support turns the global integral into its required local form.

theorem positiveSquaredDistance_source {p : X} {r R C a : ℝ} (hR : 0 ≤ R)
    (χ : GoodLaplacianCutoff μ hQ p R C) (hrR : r ≤ R) (σ : Measure X)
    (hsource : ∀ (ψ : SobolevSpace μ hQ) (v : X → ℝ) (L : ℝ≥0),
      LipschitzWith L v → HasCompactSupport v → tsupport v ⊆ ball p R →
      SobolevSpace.toLp μ hQ ψ =ᵐ[μ] v →
      energyForm μ hQ (inwardQuadratic μ hQ p hR) ψ + a * (∫ x, v x ∂μ) = ∫ x, v x ∂σ) :
    ∀ (ψ : SobolevSpace μ hQ) (v : X → ℝ) (L : ℝ≥0),
      LipschitzWith L v → HasCompactSupport v → tsupport v ⊆ ball p r →
      SobolevSpace.toLp μ hQ ψ =ᵐ[μ] v →
      energyForm μ hQ (positiveSquaredDistance μ hQ hR χ) ψ +
        a * (∫ x in ball p r, v x ∂μ) = ∫ x, v x ∂σ := by
…

Mentions: OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.inwardQuadratic, OAI.RegularPointCoordinates.positiveSquaredDistance