PositiveDistanceLocality.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.RegularPointCoordinates.positiveSquaredDistance_pairing_independent line 20
Source documentation
All positive squared-distance data at one center agree locally. Consequently their pairing with an arbitrary Sobolev direction is the same raw radial derivative, even though their compact supports differ.
```
theorem positiveSquaredDistance_pairing_independent {p : X} {r R₁ R₂ C₁ C₂ : ℝ}
    (hR₁ : 0 ≤ R₁) (hR₂ : 0 ≤ R₂) (hr₁ : r ≤ R₁) (hr₂ : r ≤ R₂)
    (χ₁ : GoodLaplacianCutoff μ hQ p R₁ C₁)
    (χ₂ : GoodLaplacianCutoff μ hQ p R₂ C₂) (a : SobolevSpace μ hQ) :
    localGamma μ hQ (positiveSquaredDistance μ hQ hR₁ χ₁) a =ᵐ[μ.restrict (ball p r)]
      localGamma μ hQ (positiveSquaredDistance μ hQ hR₂ χ₂) a := by
…
```
Mentions: OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.positiveSquaredDistance
theorem OAI.RegularPointCoordinates.distanceSourceRadius_add line 41