OAI/Probability/ClassicalON/SeparatedAnnuli.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClassicalON.LatticeGraph.annulusIndicator line 13
2. theorem OAI.ClassicalON.LatticeGraph.annulusIndicator_nonneg line 18
3. theorem OAI.ClassicalON.LatticeGraph.annulusIndicator_monotone line 22
4. theorem OAI.ClassicalON.LatticeGraph.annulusEdgesEquiv_symm_val line 30
5. theorem OAI.ClassicalON.LatticeGraph.separated_annuli_factor line 36
6. theorem OAI.ClassicalON.LatticeGraph.separated_annuli_small line 56