RadialSquaredDistance.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Applying the radial test to an actual squared-distance representative

The squared-distance function is cut off only at the larger working radius. Locality transfers its radial pairing to each smaller ball. The resulting mass estimate takes precisely the local weak Laplacian-defect identity and the eikonal input, rather than an assumed annular source formula.

theorem OAI.RegularPointCoordinates.inwardQuadratic_gamma_smaller line 25

theorem OAI.RegularPointCoordinates.squaredDistance_source_mass_le line 66

Source documentation

The actual positive squared-distance defect satisfies the volume-drop bound on an inner ball. Its two published inputs are the local weak defect identity and the distance eikonal property. Bishop--Gromov removes the sphere exception.

theorem squaredDistance_source_mass_le {n r R T curvature : ℝ}
    (hn : 0 < n) (hr : 0 < r) (hrR : r < R) (hRT : R < T)
    (hcurvature : 0 ≤ curvature) (c : X) (σ : Measure X) [IsFiniteMeasure σ]
    {model : ℝ → ℝ} (hBG : BallVolumeComparison μ model) (hmodelcont : Continuous model)
    (hmodelr : 0 < model r)
    (heik : ∀ᵐ x ∂μ, x ∈ ball c R →
      localGamma μ hQ (inwardSobolev μ hQ c R) (inwardSobolev μ hQ c R) x = 1)
    (hdefect : ∀ (ψ : SobolevSpace μ hQ) (v : X → ℝ) (C : ℝ≥0),
      LipschitzWith C v → HasCompactSupport v → tsupport v ⊆ ball c T →
      SobolevSpace.toLp μ hQ ψ =ᵐ[μ] v →
      energyForm μ hQ (inwardQuadratic μ hQ c ((hr.trans hrR).trans hRT).le) ψ +
        (n + curvature) * (∫ x, v x ∂μ) = ∫ x, v x ∂σ) :
…

Mentions: OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.inwardSobolev, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.inwardQuadratic