OAI/Geometry/RCD/Heat/GaussianCoshComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A strict curvature margin supplies the small-mesh comparison coefficient

  1. theorem OAI.RegularPointCoordinates.one_add_half_sq_le_cosh line 12
  2. theorem OAI.RegularPointCoordinates.gaussian_factor_cosh_ge_one line 22
  3. theorem OAI.RegularPointCoordinates.eventually_gaussian_cosh_comparison line 47