OAI/Geometry/WeakHessian/Calculus/DualLimits.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.lipschitz_integral_tendsto_supported line 18
2. lemma OAI.WeakHessian.squareDensity_varying_pairing_tendsto line 36
3. lemma OAI.WeakHessian.contact_integral_eq line 64
4. lemma OAI.WeakHessian.contact_of_integral_eq line 77
5. lemma OAI.WeakHessian.centered_dual_bound line 95
6. lemma OAI.WeakHessian.exists_dual_subsequence line 116