OAI/Geometry/RCD/Transport/ScaledRadialTransportGeometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Radial transport weights at arbitrary positive radius

  1. def OAI.RegularPointCoordinates.scaledTransportWeight line 16

    Source documentation

    Multiplying the annular derivative by the physical radius preserves coercivity when the working balls shrink.

    def scaledTransportWeight (n : ℕ) (R : ℝ) (z x : X) : ℝ :=
…
  2. theorem OAI.RegularPointCoordinates.scaled_transport_weight_geometry line 19
  3. theorem OAI.RegularPointCoordinates.scaled_transport_interior_weight line 102