OAI/Geometry/RCD/Harmonic/LogCoshQuadratic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The midpoint comparison for negative-curvature distortion

The logarithm of cosh divided by the square is decreasing. This gives the exact dimension interpolation needed to compare the full CD and reduced CD midpoint coefficients, rather than a Gaussian approximation.

  1. def OAI.RegularPointCoordinates.logCoshQuadraticNumerator line 16
  2. theorem OAI.RegularPointCoordinates.logCoshQuadraticNumerator_hasDerivAt line 19
  3. theorem OAI.RegularPointCoordinates.logCoshQuadraticNumerator_nonpos line 36
  4. theorem OAI.RegularPointCoordinates.log_cosh_div_sq_hasDerivAt line 50
  5. theorem OAI.RegularPointCoordinates.log_cosh_div_sq_antitone line 64
  6. theorem OAI.RegularPointCoordinates.log_cosh_sqrt_mul_ge line 74