OAI/Probability/SKGap/Localization/TruncationGoodSet.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.truncationGoodSet line 48
2. lemma OAI.SKGap.truncationGoodSet_measurable line 53
3. lemma OAI.SKGap.realTruncatedK_lipschitz line 62
4. lemma OAI.SKGap.goeMatrix_transpose line 73
5. lemma OAI.SKGap.symmetricElementary_transpose line 79
6. lemma OAI.SKGap.realTruncatedK_goe_derivative line 83
7. theorem OAI.SKGap.realTruncatedK_first_loop line 95