OAI/Geometry/WeakHessian/Entropy/FisherEpsilon.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakHessian.renormalizedEntropy_integrable line 53
  2. lemma OAI.WeakHessian.integral_renormalizedEntropy line 58
  3. lemma OAI.WeakHessian.CurvatureDimension.cheegerHeat_renormalizedEntropy_FTC line 64
  4. lemma OAI.WeakHessian.CurvatureDimension.cheegerHeat_regularizedFisher_action_bound line 75
  5. def OAI.WeakHessian.fisherEpsilon line 125
  6. lemma OAI.WeakHessian.fisherEpsilon_pos line 126
  7. lemma OAI.WeakHessian.fisherEpsilon_le_one line 127
  8. lemma OAI.WeakHessian.fisherEpsilon_antitone line 130
  9. lemma OAI.WeakHessian.fisherEpsilon_tendsto line 134
  10. lemma OAI.WeakHessian.regularizedFisher_mono line 137
  11. lemma OAI.WeakHessian.regularizedFisher_tendsto line 144
  12. lemma OAI.WeakHessian.ofReal_fisher_eq_iSup line 152
  13. lemma OAI.WeakHessian.integrable_regularizedFisher line 158
  14. lemma OAI.WeakHessian.lintegral_fisher_eq_iSup line 167
  15. lemma OAI.WeakHessian.fisher_action_of_regularization line 186
  16. lemma OAI.WeakHessian.integral_regularizedFisher_tendsto line 234
  17. lemma OAI.WeakHessian.integral_regularizedFisher_action_tendsto line 243