InwardDistance.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Compact inward distance and its squared-distance primitive

The inward distance to the boundary of a metric ball is a compactly supported Lipschitz function. Its quadratic primitive agrees with squared distance, up to a constant, on the ball. This realizes radial tests in the global Sobolev space without pretending the unbounded distance itself is in L2.

def OAI.RegularPointCoordinates.inwardDistance line 25
theorem OAI.RegularPointCoordinates.inwardDistance_lipschitz line 28
theorem OAI.RegularPointCoordinates.inwardDistance_compact line 38
def OAI.RegularPointCoordinates.inwardSobolev line 45
theorem OAI.RegularPointCoordinates.inwardSobolev_coe line 48
theorem OAI.RegularPointCoordinates.inwardSobolev_bounds line 52
def OAI.RegularPointCoordinates.inwardQuadratic line 60
Source documentation
The primitive equals dist²/2 - R²/2 inside the ball.
```
def inwardQuadratic (c : X) {R : ℝ} (hR : 0 ≤ R) : SobolevSpace μ hQ :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.inwardQuadratic_coe line 64
theorem OAI.RegularPointCoordinates.inwardQuadratic_gamma line 87
Source documentation
Eikonal control of inward distance gives the required radial pairing. The eikonal premise is the local distance consequence of Gigli (2015), Corollary 5.15 and Theorem 5.3; it is not a source-mass estimate.
```
theorem inwardQuadratic_gamma (c : X) {R : ℝ} (hR : 0 ≤ R)
    (heik : ∀ᵐ x ∂μ, x ∈ ball c R →
      localGamma μ hQ (inwardSobolev μ hQ c R) (inwardSobolev μ hQ c R) x = 1) :
    ∀ᵐ x ∂μ, x ∈ ball c R →
      localGamma μ hQ (inwardQuadratic μ hQ c hR) (inwardSobolev μ hQ c R) x = -dist c x := by
…
```
Mentions: OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.inwardSobolev, OAI.RegularPointCoordinates.inwardQuadratic