OAI/Probability/SKGap/Localization/SeparateCut.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.Noncrossing.Diagram.separateCut line 13
2. def OAI.SKGap.Noncrossing.Diagram.joinCut line 17
3. lemma OAI.SKGap.Noncrossing.Diagram.join_separate line 27
4. lemma OAI.SKGap.Noncrossing.Diagram.pair_heq line 34
5. lemma OAI.SKGap.Noncrossing.Diagram.separate_join line 40
6. def OAI.SKGap.Noncrossing.Diagram.separateEquiv line 55
7. def OAI.SKGap.Noncrossing.Diagram.mean line 64
8. def OAI.SKGap.Noncrossing.Diagram.value line 66
9. lemma OAI.SKGap.Noncrossing.Diagram.mean_const_mul line 71
10. lemma OAI.SKGap.Noncrossing.Diagram.value_insert line 75
11. lemma OAI.SKGap.Noncrossing.Diagram.value_cut line 92
12. def OAI.SKGap.Noncrossing.Diagram.prediction line 98
13. lemma OAI.SKGap.Noncrossing.Diagram.mean_prediction line 101
14. theorem OAI.SKGap.Noncrossing.Diagram.prediction_cut line 106