OAI/Geometry/RCD/Metric/DimensionalRatePair.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Pairing the two dimensional evolution rates

The entropy ratios cancel by the weighted arithmetic-geometric mean inequality. The remaining error records the difference of the square roots of the two time speeds.

  1. theorem OAI.RegularPointCoordinates.hyperbolic_rate_quadratic_bound line 17
  2. theorem OAI.RegularPointCoordinates.weighted_entropy_ratio_ge line 44
  3. theorem OAI.RegularPointCoordinates.dimensional_rate_pair line 55