OAI/Geometry/WeakHessian/Geodesics/MidpointSigmaLower.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakHessian.midpointSigmaLower line 45
  2. lemma OAI.WeakHessian.midpointSigmaLower_pos line 48
  3. lemma OAI.WeakHessian.midpointSigmaLower_le_half line 52
  4. lemma OAI.WeakHessian.midpoint_sin_ratio line 59
  5. lemma OAI.WeakHessian.midpoint_sinh_ratio line 71
  6. lemma OAI.WeakHessian.sigmaCoeff_midpoint_lower line 87
  7. def OAI.WeakHessian.midpointTauLower line 127
  8. lemma OAI.WeakHessian.midpointTauLower_pos line 131
  9. lemma OAI.WeakHessian.midpointTauLower_ne_top line 138
  10. lemma OAI.WeakHessian.tauCoeff_midpoint_lower line 146
  11. lemma OAI.WeakHessian.renyiIntegral_le_support line 156
  12. def OAI.WeakHessian.normalizedRestriction line 193
  13. lemma OAI.WeakHessian.normalizedRestriction_ac line 197
  14. lemma OAI.WeakHessian.normalizedRestriction_ae_mem line 202
  15. lemma OAI.WeakHessian.normalizedRestriction_probability line 207
  16. lemma OAI.WeakHessian.interpolation_probability line 213
  17. lemma OAI.WeakHessian.sigmaFinite_of_finiteOnBoundedSets line 219
  18. lemma OAI.WeakHessian.rnDeriv_normalizedRestriction line 228
  19. lemma OAI.WeakHessian.hasSecondMoment_of_ae_dist_le line 240
  20. lemma OAI.WeakHessian.cd_midpoint_ball_volume line 251
  21. lemma OAI.WeakHessian.cd_iterated_ball_volume line 337
  22. lemma OAI.WeakHessian.cd_uniform_ball_measure_lower line 362
  23. lemma OAI.WeakHessian.properSpace_of_cd line 400