OAI/Probability/SKGap/Localization/NoiseSplit.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SKGap.Noncrossing.Diagram.NoiseSplit line 21
2. lemma OAI.SKGap.Noncrossing.Diagram.NoiseSplit.before_take line 26
3. lemma OAI.SKGap.Noncrossing.Diagram.NoiseSplit.after_drop line 29
4. lemma OAI.SKGap.Noncrossing.Diagram.NoiseSplit.length_bound line 32
5. def OAI.SKGap.Noncrossing.Diagram.NoiseSplit.code line 38
6. lemma OAI.SKGap.Noncrossing.Diagram.NoiseSplit.code_injective line 40
7. instance OAI.SKGap.Noncrossing.Diagram.noiseSplitFinite line 47
8. instance OAI.SKGap.Noncrossing.Diagram.noiseSplitFintype line 49
9. def OAI.SKGap.Noncrossing.Diagram.shapeAt line 52
10. lemma OAI.SKGap.Noncrossing.Diagram.shapeAt_bijective line 61
11. def OAI.SKGap.Noncrossing.Diagram.shapeAtEquiv line 97
12. def OAI.SKGap.Noncrossing.Diagram.evaluate line 104
13. lemma OAI.SKGap.Noncrossing.Diagram.evaluate_nil line 106
14. lemma OAI.SKGap.Noncrossing.Diagram.evaluate_diag line 108
15. lemma OAI.SKGap.Noncrossing.Diagram.evaluate_arch line 110
16. lemma OAI.SKGap.Noncrossing.Diagram.evaluate_insert line 113
17. def OAI.SKGap.Noncrossing.Diagram.expect line 131
18. lemma OAI.SKGap.Noncrossing.Diagram.mean_expect line 134
19. lemma OAI.SKGap.Noncrossing.Diagram.expect_cut line 139
20. theorem OAI.SKGap.Noncrossing.Diagram.expect_at line 168