OAI/Probability/SKBarriers/Locking/FourBlockTent.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SK.Analytic.fourBlockTent line 14
2. theorem OAI.SK.Analytic.fourBlockTent_length line 17
3. abbrev OAI.SK.Analytic.fourBlockLeft line 22
4. abbrev OAI.SK.Analytic.fourBlockMiddle line 24
5. abbrev OAI.SK.Analytic.fourBlockRight line 26
6. theorem OAI.SK.Analytic.fourBlockTent_vector line 29
7. theorem OAI.SK.Analytic.fourBlockTent_left_variance line 66
8. theorem OAI.SK.Analytic.fourBlockTent_middle_variance line 74
9. theorem OAI.SK.Analytic.fourBlockTent_right_variance line 82