OAI/Analysis/MatrixSigning/Potential/EndpointCandidates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CurrentKS.State.LightPoint.computed_candidates_progress line 17
2. lemma OAI.CurrentKS.RationalRoot.computedCurvature_norm line 72
3. lemma OAI.CurrentKS.Difference.interiorCandidates_distance line 95
4. def OAI.CurrentKS.Difference.endpointCandidates line 118
5. def OAI.CurrentKS.Difference.allCandidates line 121
6. lemma OAI.CurrentKS.Difference.endpoint_mem line 125
7. lemma OAI.CurrentKS.Difference.endpointCandidates_cube line 133
8. lemma OAI.CurrentKS.Difference.allCandidates_cube line 144