RadialTransport.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The outer-ball estimate for an unnormalized radial residual

theorem OAI.RegularPointCoordinates.radial_transport_outer_from_energy line 19
Source documentation
Positivity of the actual cutoff converts annular energy to the larger-ball norm. The inner sphere is harmless under Bishop--Gromov.
```
theorem radial_transport_outer_from_energy {n : ℕ} {R : ℝ} (hR : 2 ≤ R)
    (z : X) {w : X → ℝ} (hw : MemLp w 2 μ) (hsphere : μ (sphere z R) = 0) :
    let β := transportCutoffExponent n
…
```
Mentions: OAI.RegularPointCoordinates.transportCutoffExponent

theorem OAI.RegularPointCoordinates.radial_transport_squared line 67

Source documentation

Quantitative radial transport in its squared-norm form. Both error terms stay quadratic, and all constants are independent of the residual's possibly tiny inner norm.

theorem radial_transport_squared {n : ℕ} {R a : ℝ} (hR : 2 ≤ R)
    (ha : 0 ≤ a) (han : a ≤ (n : ℝ) + 1) (z : X)
    (f w : SobolevSpace μ hQ)
    (hf : IsConstantLaplacianOn μ hQ (ball z (4 * R)) f a)
    (C : ℝ≥0) (hw : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ w x| ≤ C)
    (F e : X → ℝ) (hF : MemLp F 2 μ) (he : MemLp e 2 μ)
    (heuler : localGamma μ hQ f w =ᵐ[μ.restrict (ball z (4 * R))]
      fun x => SobolevSpace.toLp μ hQ w x + F x / 2)
    (hradial : localGamma μ hQ f (inwardSobolev μ hQ z (3 * R))
      =ᵐ[μ.restrict (ball z (4 * R))] fun x => e x - dist z x)
    (hsphere : μ (sphere z R) = 0) :
    let β := transportCutoffExponent n
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.inwardSobolev, OAI.RegularPointCoordinates.transportCutoffExponent