OAI/Analysis/MatrixSigning/Potential/RationalBasis.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.Difference.rationalBasis line 14
2. def OAI.CurrentKS.Difference.realBasis line 15
3. def OAI.CurrentKS.Difference.pointCast line 17
4. lemma OAI.CurrentKS.Difference.pointCast_step line 19
5. lemma OAI.CurrentKS.Difference.pointCast_basis line 24
6. lemma OAI.CurrentKS.Difference.pointCast_add line 28
7. lemma OAI.CurrentKS.Difference.pointCast_neg line 32
8. lemma OAI.CurrentKS.Difference.realBasis_bound line 36
9. def OAI.CurrentKS.Difference.stencilValue line 41
10. def OAI.CurrentKS.Difference.stencilGradient line 44
11. def OAI.CurrentKS.Difference.stencilHessian line 47
12. lemma OAI.CurrentKS.Difference.stencilHessian_symm line 56
13. lemma OAI.CurrentKS.Difference.ball_remainder_unit line 72
14. theorem OAI.CurrentKS.Difference.stencilGradient_error line 83
15. theorem OAI.CurrentKS.Difference.stencilHessian_diagonal_error line 108
16. lemma OAI.CurrentKS.Difference.pointCast_sub line 135
17. lemma OAI.CurrentKS.Difference.realBasis_pair_bound line 139
18. theorem OAI.CurrentKS.Difference.stencilHessian_mixed_error line 147