OAI/Probability/BenjaminiSchramm/BoundedLayerShift.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Percolation.BenjaminiSchramm.restrictedLayerCount_expectation_le_row_bound line 14
  2. theorem OAI.Percolation.BenjaminiSchramm.first_layer_moment_bound_with_row line 26
  3. lemma OAI.CriticalPercolation.BondGraph.adjustedCeilingBandCount_eq_restrictedLayerCount line 66
  4. theorem OAI.CriticalPercolation.BondGraph.expected_ceilingBandCount_le_intermediate_upLayerMoment line 79