OAI/Probability/BenjaminiSchramm/LayerFrontierExpectation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Percolation.BenjaminiSchramm.newLayerCount line 12
2. def OAI.Percolation.BenjaminiSchramm.frontierCount line 15
3. lemma OAI.Percolation.BenjaminiSchramm.measurable_newLayerCount line 18
4. lemma OAI.Percolation.BenjaminiSchramm.measurable_frontierCount line 27
5. lemma OAI.Percolation.BenjaminiSchramm.newLayerCount_eq_on_cell line 39
6. lemma OAI.Percolation.BenjaminiSchramm.frontierCount_eq_card_on_cell line 50
7. theorem OAI.Percolation.BenjaminiSchramm.lintegral_lowerFrontier_partition line 62
8. theorem OAI.Percolation.BenjaminiSchramm.newLayerCount_fractional_bound_on_frontier line 96
9. theorem OAI.Percolation.BenjaminiSchramm.newLayerCount_fractional_bound line 151