OAI/Geometry/WeakHessian/Calculus/FormLimits.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.form_cauchySchwarz line 21
2. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.scaled_resolvent_energy_le line 25
3. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.scaled_resolvent_energy_tendsto line 30
4. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.scaled_resolvent_form_error_le line 44
5. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.exists_formGenerator_approx line 66
6. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.form_tendsto_zero_of_bounded_energy line 80
7. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.form_tendsto_of_bounded_energy line 115
8. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.form_energy_sub_tendsto line 131