OAI/Geometry/RCD/Transport/MidpointReducedComparison.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The reduced midpoint coefficient is bounded by the full CD coefficient

  1. theorem OAI.RegularPointCoordinates.sigma_negative_midpoint line 12
  2. theorem OAI.RegularPointCoordinates.reduced_midpoint_le_tau_negative line 21
  3. theorem OAI.RegularPointCoordinates.sin_half_div_sin_exact line 45
  4. theorem OAI.RegularPointCoordinates.sigma_positive_midpoint line 56
  5. theorem OAI.RegularPointCoordinates.reduced_midpoint_le_tau_positive line 66