OAI/Geometry/RCD/Transport/RadialTransportCutoffBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Positive interior weight of the radial transport cutoff

  1. theorem OAI.RegularPointCoordinates.radial_transport_cutoff_lower line 16

    Source documentation

    The fixed transport cutoff is uniformly positive through radius 2R, although it vanishes outside radius 3R.

    theorem radial_transport_cutoff_lower {n : ℕ} {R : ℝ} (hR : 2 ≤ R) (z : X) :
    let β := transportCutoffExponent n
…

    Mentions: OAI.RegularPointCoordinates.transportCutoffExponent