OAI/Geometry/RCD/Transport/HyperbolicDistortion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Sharp radial distortion on bounded annuli

The curvature-dimension coefficients retain their hyperbolic radial factor. These scalar comparisons will be used with the actual transport plan to compare annuli before integrating the radial volume density.

  1. theorem OAI.RegularPointCoordinates.sinh_mul_cosh_sub_nonneg line 17
  2. theorem OAI.RegularPointCoordinates.monotone_hyperbolic_radial_logDerivative line 33
  3. theorem OAI.RegularPointCoordinates.antitone_sinh_radial_ratio line 54
  4. theorem OAI.RegularPointCoordinates.sinh_radial_ratio_le_time line 85
  5. theorem OAI.RegularPointCoordinates.sigma_neg_eq line 100
  6. theorem OAI.RegularPointCoordinates.sigma_antitone_distance_nonpos_curvature line 112
  7. theorem OAI.RegularPointCoordinates.tau_antitone_distance_nonpos_curvature line 135
  8. theorem OAI.RegularPointCoordinates.tau_nat_power line 144