RadialTransportCutoff.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A radial power cutoff with the transport sign

The power cutoff has a compact Sobolev representative and exact chain rule. Taking exponent 2(n+4) gives the sign needed for radial transport whenever the fixed inner radius is at least two.

def OAI.RegularPointCoordinates.transportCutoffExponent line 17
theorem OAI.RegularPointCoordinates.transportCutoffExponent_pos line 19
theorem OAI.RegularPointCoordinates.radial_transport_power_sign line 25
Source documentation
The actual negative radial derivative dominates both its own size and the zeroth-order transport coefficient throughout the outer annulus.
```
theorem radial_transport_power_sign {n : ℕ} {a R t : ℝ}
    (hR : 2 ≤ R) (ht : R ≤ t) (ha : 0 ≤ a) (han : a ≤ (n : ℝ) + 1) :
    let β := transportCutoffExponent n
…
```
Mentions: OAI.RegularPointCoordinates.transportCutoffExponent

theorem OAI.RegularPointCoordinates.radial_transport_cutoff_sign line 64

Source documentation

The radial power cutoff satisfies the coercive transport sign.

theorem radial_transport_cutoff_sign {n : ℕ} {a R : ℝ}
    (hR : 2 ≤ R) (ha : 0 ≤ a) (han : a ≤ (n : ℝ) + 1) (z x : X)
    (hinner : R ≤ dist z x) (houter : dist z x ≤ 3 * R) :
    let β := transportCutoffExponent n
…

Mentions: OAI.RegularPointCoordinates.transportCutoffExponent