OAI/Probability/BenjaminiSchramm/NormalizedHalfspace.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.adjustedHalfspaceHit line 14
2. def OAI.CriticalPercolation.BondGraph.infimalAdjustedCrossing line 18
3. lemma OAI.CriticalPercolation.BondGraph.adjustedHalfspaceHit_zero line 21
4. lemma OAI.CriticalPercolation.BondGraph.infimalAdjustedCrossing_zero line 27
5. lemma OAI.CriticalPercolation.BondGraph.adjustedHalfspaceHit_upper line 31
6. lemma OAI.CriticalPercolation.BondGraph.adjustedHalfspaceHit_finiteWitness line 36
7. lemma OAI.CriticalPercolation.BondGraph.adjustedHalfspaceHit_hasFiniteOpenWitness line 45
8. lemma OAI.CriticalPercolation.BondGraph.measurableSet_adjustedHalfspaceHit line 51
9. lemma OAI.CriticalPercolation.BondGraph.Aut.adjustedHalfspaceHit_preimage line 56
10. lemma OAI.CriticalPercolation.BondGraph.Aut.adjustedHalfspaceHit_measure line 84
11. lemma OAI.CriticalPercolation.BondGraph.infimalAdjustedCrossing_le_one line 92
12. theorem OAI.CriticalPercolation.BondGraph.infimalAdjustedCrossing_supermultiplicative line 96