OAI/Geometry/WeakHessian/Entropy/ZeroDensity.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakHessian.squareDensityMeasure line 22
  2. lemma OAI.WeakHessian.squareDensity_integral line 26
  3. lemma OAI.WeakHessian.squareDensity_integrable line 33
  4. lemma OAI.WeakHessian.squareDensity_inv_integrable line 40
  5. lemma OAI.WeakHessian.squareDensity_inv_mass line 50
  6. lemma OAI.WeakHessian.squareDensity_pos_ae line 62
  7. def OAI.WeakHessian.squareLogFloor line 70
  8. lemma OAI.WeakHessian.squareLogFloor_eq line 74
  9. lemma OAI.WeakHessian.squareLogFloor_lipschitz line 79
  10. def OAI.WeakHessian.squareLogFloorBCF line 90
  11. lemma OAI.WeakHessian.squareLogFloorBCF_apply line 95
  12. lemma OAI.WeakHessian.exp_squareLogFloor line 99
  13. lemma OAI.WeakHessian.squareDensity_entropy_upper line 103
  14. lemma OAI.WeakHessian.squareDensity_mass line 138
  15. lemma OAI.WeakHessian.squareDensity_fenchel_defect line 143
  16. lemma OAI.WeakHessian.squareLogFloor_increment_comparison line 165
  17. lemma OAI.WeakHessian.entropy_chord_squareRoot_approx line 217
  18. lemma OAI.WeakHessian.gamma_squareLogFloor line 291
  19. lemma OAI.WeakHessian.integrable_local_gamma_finite_ac line 310
  20. lemma OAI.WeakHessian.squareLogFloor_contact_upper line 323
  21. lemma OAI.WeakHessian.IsTestPlan.entropy_squareRoot_subdifferential line 378