RadialPowerTest.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Radial inverse-power tests

A bounded continuous weight is integrated before clipping the argument. The resulting Sobolev test has the exact annular derivative needed to convert the squared-distance weak Laplacian into a volume drop.

def OAI.RegularPointCoordinates.radialPowerWeight line 22
Source documentation
The global derivative used before clipping at the inner radius.
```
def radialPowerWeight (n r R s : ℝ) : ℝ := (max r (R - s)) ^ (-(n + 1))
```
def OAI.RegularPointCoordinates.radialPowerPrimitive line 24
theorem OAI.RegularPointCoordinates.radialPowerWeight_continuous line 27
theorem OAI.RegularPointCoordinates.radialPowerWeight_bounds line 34
theorem OAI.RegularPointCoordinates.radialPowerPrimitive_hasDerivAt line 40
theorem OAI.RegularPointCoordinates.radialPowerPrimitive_zero line 47
theorem OAI.RegularPointCoordinates.radialPowerPrimitive_lipschitz line 50
theorem OAI.RegularPointCoordinates.radialPowerPrimitive_formula line 63
Source documentation
On the unclipped interval this primitive is the inverse-power cutoff.
```
theorem radialPowerPrimitive_formula {n r R s : ℝ} (hn : 0 < n) (hr : 0 < r)
    (hs : 0 ≤ s) (hsR : s ≤ R - r) :
    radialPowerPrimitive n r R s = ((R - s) ^ (-n) - R ^ (-n)) / n := by
…
```
Mentions: OAI.RegularPointCoordinates.radialPowerPrimitive
theorem OAI.RegularPointCoordinates.positiveTruncation_gamma_pair line 95
Source documentation
Clipping has the same locality formula when paired with any Sobolev function.
```
theorem positiveTruncation_gamma_pair (q u : SobolevSpace μ hQ)
    (hu : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ u x) {t : ℝ} (ht : 0 ≤ t) :
    localGamma μ hQ q (positiveTruncation μ hQ u t ht) =ᵐ[μ]
      fun x => if SobolevSpace.toLp μ hQ u x < t then localGamma μ hQ q u x else 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.positiveTruncation
def OAI.RegularPointCoordinates.radialPowerTest line 114
Source documentation
The actual radial Sobolev test obtained by clipping an inward distance.
```
def radialPowerTest (u : SobolevSpace μ hQ) {n r R : ℝ}
    (hn : 0 < n) (hr : 0 < r) (hrR : r ≤ R) : SobolevSpace μ hQ :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.radialPowerTest_coe line 121
theorem OAI.RegularPointCoordinates.radialPowerTest_gamma line 130