OAI/Geometry/WeakHessian/Transport/AeEvalAe.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.IsTestPlan.ae_eval_of_ae line 19
2. lemma OAI.WeakHessian.continuous_clampTime line 27
3. lemma OAI.WeakHessian.continuous_evalReal line 31
4. lemma OAI.WeakHessian.IsTestPlan.ae_ae_eval_of_ae line 34
5. lemma OAI.WeakHessian.LocallyL2.ae_eq line 57
6. lemma OAI.WeakHessian.IsLocalWeakUpperGradient.congr_ae line 62
7. lemma OAI.WeakHessian.IsMinimalLocalWeakUpperGradient.congr_ae line 85
8. lemma OAI.WeakHessian.exists_isMinimal_congr_ae line 94
9. lemma OAI.WeakHessian.weakGradient_congr_ae line 103
10. lemma OAI.WeakHessian.localSobolev_congr_ae line 113
11. lemma OAI.WeakHessian.sobolev_congr_ae line 118
12. lemma OAI.WeakHessian.gamma_congr_ae line 128