RadialCutoffMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Source mass from the squared-distance weak identity

Gigli (2015), Corollary 5.15, equation (5.29), supplies the local positive Laplacian defect of squared distance. Applying that defect to the explicit radial test gives this volume-drop bound directly. The only calculus premise is the actual radial pairing, obtained from the distance eikonal identity; no mass bound or radial distribution identity is assumed.

theorem OAI.RegularPointCoordinates.radialPowerRep_bounds line 24
theorem OAI.RegularPointCoordinates.radialPowerRep_tsupport line 46
Source documentation
The radial test has support strictly inside any larger working ball.
```
theorem radialPowerRep_tsupport {n r R T : ℝ} (hrR : r ≤ R) (hRT : R < T) (c : X) :
    tsupport (radialPowerRep n r R c) ⊆ ball c T := by
…
```
Mentions: OAI.RegularPointCoordinates.radialPowerRep

theorem OAI.RegularPointCoordinates.radial_source_cutoff_mass_le line 59

Source documentation

The positive squared-distance Laplacian defect has an annular volume budget, with an explicit coefficient and curvature term.

theorem radial_source_cutoff_mass_le {n r R T curvature : ℝ}
    (hn : 0 < n) (hr : 0 < r) (hrR : r < R) (hRT : R < T)
    (hcurvature : 0 ≤ curvature) (c : X) (q : SobolevSpace μ hQ)
    (σ : Measure X) [IsFiniteMeasure σ]
    (hdefect : ∀ (ψ : SobolevSpace μ hQ) (v : X → ℝ) (C : ℝ≥0),
      LipschitzWith C v → HasCompactSupport v → tsupport v ⊆ ball c T →
      SobolevSpace.toLp μ hQ ψ =ᵐ[μ] v →
      energyForm μ hQ q ψ + (n + curvature) * (∫ x, v x ∂μ) = ∫ x, v x ∂σ)
    (hpair : ∀ᵐ x ∂μ, x ∈ ball c R →
      localGamma μ hQ q (inwardSobolev μ hQ c R) x = -dist c x)
    (hsphere : μ (sphere c r) = 0) :
    ((r ^ (-n) - R ^ (-n)) / n) * σ.real (ball c r) ≤
…

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