OAI/Geometry/WeakHessian/Entropy/FisherDensity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.weakGradient_zero_on_zero line 49
2. lemma OAI.WeakHessian.weakGradient_le_localSlope line 57
3. lemma OAI.WeakHessian.fisher_young line 63
4. def OAI.WeakHessian.fisherDensity line 72
5. lemma OAI.WeakHessian.weakGradient_le_fisher line 74
6. lemma OAI.WeakHessian.integrable_gradient_of_fisher line 83
7. lemma OAI.WeakHessian.gamma_fisher_young line 91
8. lemma OAI.WeakHessian.integrable_density_slope_sq line 107
9. lemma OAI.WeakHessian.IsLaplacian.fisher_pairing line 118