RadialCutoffIdentity.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Exact volume-drop identity for the radial test

The weak squared-distance pairing is integrated against the explicit radial power test. Its combination with n times the test is exactly the difference of the two normalized ball indicators. Positive source mass will therefore be controlled by the actual volume drop, including its sign.

def OAI.RegularPointCoordinates.radialPowerRep line 26
Source documentation
The continuous representative of the Sobolev radial test.
```
def radialPowerRep (n r R : ℝ) (c : X) (x : X) : ℝ :=
…
```
theorem OAI.RegularPointCoordinates.radialPowerRep_lipschitz line 30
theorem OAI.RegularPointCoordinates.radialPowerRep_compact line 40
theorem OAI.RegularPointCoordinates.radialPowerRep_zero line 46
theorem OAI.RegularPointCoordinates.radialPowerRep_inner line 52
theorem OAI.RegularPointCoordinates.radialPowerRep_annulus line 61
theorem OAI.RegularPointCoordinates.radialPowerTest_inward_coe line 72

theorem OAI.RegularPointCoordinates.radialPowerTest_indicator_identity line 82

Source documentation

The pointwise cancellation on the annulus, and constancy on the inner ball.

theorem radialPowerTest_indicator_identity {n r R : ℝ} (hn : 0 < n) (hr : 0 < r)
    (hrR : r < R) (c : X) (q : SobolevSpace μ hQ)
    (hpair : ∀ᵐ x ∂μ, x ∈ ball c R →
      localGamma μ hQ q (inwardSobolev μ hQ c R) x = -dist c x)
    (hsphere : μ (sphere c r) = 0) :
    (fun x => n * radialPowerRep n r R c x +
      localGamma μ hQ q (radialPowerTest μ hQ (inwardSobolev μ hQ c R) hn hr hrR.le) x) =ᵐ[μ]
      fun x => (ball c r).indicator (fun _ => r ^ (-n)) x -
        (ball c R).indicator (fun _ => R ^ (-n)) x := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.inwardSobolev, OAI.RegularPointCoordinates.radialPowerRep, OAI.RegularPointCoordinates.radialPowerTest

theorem OAI.RegularPointCoordinates.radialPowerTest_volume_identity line 137

Source documentation

Integrating the cancellation gives the actual normalized volume drop.

theorem radialPowerTest_volume_identity {n r R : ℝ} (hn : 0 < n) (hr : 0 < r)
    (hrR : r < R) (c : X) (q : SobolevSpace μ hQ)
    (hpair : ∀ᵐ x ∂μ, x ∈ ball c R →
      localGamma μ hQ q (inwardSobolev μ hQ c R) x = -dist c x)
    (hsphere : μ (sphere c r) = 0) :
    n * (∫ x, radialPowerRep n r R c x ∂μ) +
      energyForm μ hQ q (radialPowerTest μ hQ (inwardSobolev μ hQ c R) hn hr hrR.le) =
      r ^ (-n) * μ.real (ball c r) - R ^ (-n) * μ.real (ball c R) := by
…