OAI/Geometry/RCD/Transport/RadialTransportGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.transportEnergyWeight line 14
2. theorem OAI.RegularPointCoordinates.radial_transport_weight_geometry line 20

   Source documentation

   The sign and the two comparisons needed by the energy argument hold for the constructed weights. Only the inner sphere is excluded.

   theorem radial_transport_weight_geometry {n : ℕ} {R a : ℝ} (hR : 2 ≤ R)
       (ha : 0 ≤ a) (han : a ≤ (n : ℝ) + 1) (z x : X) (hne : dist z x ≠ R) :
       let β := transportCutoffExponent n
   …

   Mentions: OAI.RegularPointCoordinates.transportCutoffExponent

3. theorem OAI.RegularPointCoordinates.radial_transport_interior_weight line 83

   Source documentation

   The positive cutoff controls the desired larger ball by the inner ball and the same annular energy.

   theorem radial_transport_interior_weight {n : ℕ} {R : ℝ} (hR : 2 ≤ R)
       (z x : X) (hne : dist z x ≠ R) :
       let β := transportCutoffExponent n
   …

   Mentions: OAI.RegularPointCoordinates.transportCutoffExponent

4. theorem OAI.RegularPointCoordinates.transportEnergyWeight_measurable line 117