OAI/Analysis/MatrixSigning/Potential/EuclideanForget.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CurrentKS.Difference.symmetric_bilinear_norm_le line 13
2. def OAI.CurrentKS.Difference.euclideanForget line 34
3. lemma OAI.CurrentKS.Difference.euclideanForget_apply line 37
4. lemma OAI.CurrentKS.Difference.euclideanForget_bound line 39
5. def OAI.CurrentKS.Difference.euclideanBilinear line 44
6. lemma OAI.CurrentKS.Difference.euclideanBilinear_apply line 49
7. theorem OAI.CurrentKS.Difference.actual_hessian_norm line 52
8. def OAI.CurrentKS.Difference.interiorCandidates line 73
9. lemma OAI.CurrentKS.Difference.gradient_mem_candidates line 82
10. lemma OAI.CurrentKS.Difference.curvature_mem_candidates line 87
11. lemma OAI.CurrentKS.Difference.rationalVector_forget line 92
12. lemma OAI.CurrentKS.Difference.pointCast_gradient line 94
13. theorem OAI.CurrentKS.Difference.interiorCandidates_progress line 100