OAI/Probability/SKGap/Localization/SandShift.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.ComplexMatrix.sandShift line 34
2. lemma OAI.SKGap.ComplexMatrix.sandShift_hermitian line 37
3. lemma OAI.SKGap.ComplexMatrix.sandShift_sub line 41
4. lemma OAI.SKGap.ComplexMatrix.sandShift_lipschitz line 44
5. lemma OAI.SKGap.ComplexMatrix.sandShift_parameter line 49
6. lemma OAI.SKGap.ComplexMatrix.sandShift_four_point line 60
7. lemma OAI.SKGap.ComplexMatrix.schwartzMatrix_sandShift_lipschitz line 68
8. lemma OAI.SKGap.ComplexMatrix.schwartzMatrix_sandShift_four_point line 77
9. structure OAI.SKGap.ClosedConvexNonempty line 116
10. def OAI.SKGap.convexProject line 121
11. lemma OAI.SKGap.convexProject_mem line 124
12. lemma OAI.SKGap.convexProject_minimal line 128
13. lemma OAI.SKGap.convexProject_inner line 132
14. lemma OAI.SKGap.convexProject_lipschitz line 138
15. lemma OAI.SKGap.convexProject_eq_self line 156
16. lemma OAI.SKGap.convexProject_unique line 163
17. lemma OAI.SKGap.convexProject_equivariant line 177