OAI/Geometry/RCD/Transport/MidpointDimensionAlgebra.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Scalar algebra for the full-to-reduced midpoint comparison

  1. theorem OAI.RegularPointCoordinates.half_power_reciprocal line 12
  2. theorem OAI.RegularPointCoordinates.dimension_scaled_sqrt line 19
  3. theorem OAI.RegularPointCoordinates.cosh_dimension_rpow line 27
  4. theorem OAI.RegularPointCoordinates.cos_dimension_rpow line 33
  5. theorem OAI.RegularPointCoordinates.tau_midpoint_of_sigma line 45