OAI/Analysis/MatrixSigning/Potential/ChooseCoordinate.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.Difference.chooseCoordinate line 14
2. lemma OAI.CurrentKS.Difference.chooseCoordinate_max line 17
3. theorem OAI.CurrentKS.Difference.chosen_gradient line 23
4. lemma OAI.CurrentKS.Difference.gradient_decrease line 51
5. lemma OAI.CurrentKS.Difference.opposite_decrease line 59
6. def OAI.CurrentKS.Difference.rationalGradientDirection line 76
7. def OAI.CurrentKS.Difference.gradientDirection line 79
8. lemma OAI.CurrentKS.Difference.rationalGradientDirection_cast line 82
9. lemma OAI.CurrentKS.Difference.gradientDirection_bound line 90
10. lemma OAI.CurrentKS.Difference.gradientDirection_derivative line 99
11. theorem OAI.CurrentKS.Difference.gradient_candidate_decrease line 117
12. theorem OAI.CurrentKS.Difference.opposite_candidates_decrease line 133