OAI/Probability/ClassicalON/CoarseTail.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClassicalON.LatticeGraph.codeEvent line 9
2. theorem OAI.ClassicalON.LatticeGraph.codeEvent_nonneg line 14
3. def OAI.ClassicalON.LatticeGraph.connectionProbability line 18
4. theorem OAI.ClassicalON.LatticeGraph.connectionProbability_le_one line 22
5. theorem OAI.ClassicalON.LatticeGraph.connection_le_codeSum line 32
6. theorem OAI.ClassicalON.LatticeGraph.connection_geometric_tail line 50