OAI/Geometry/RCD/Harmonic/LogCosQuadratic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The midpoint dimension comparison before the conjugate radius

  1. def OAI.RegularPointCoordinates.logCosQuadraticNumerator line 12
  2. theorem OAI.RegularPointCoordinates.logCosQuadraticNumerator_hasDerivAt line 15
  3. theorem OAI.RegularPointCoordinates.logCosQuadraticNumerator_nonpos line 27
  4. theorem OAI.RegularPointCoordinates.log_cos_div_sq_hasDerivAt line 43
  5. theorem OAI.RegularPointCoordinates.log_cos_div_sq_antitone line 56
  6. theorem OAI.RegularPointCoordinates.log_cos_sqrt_mul_ge line 69