OAI/Probability/CriticalPercolation/GraphGeometry/EllipseLinear.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.EllipseLinear.det line 13
  2. def OAI.CriticalPercolation.EllipseLinear.time line 15
  3. def OAI.CriticalPercolation.EllipseLinear.height line 17
  4. lemma OAI.CriticalPercolation.EllipseLinear.center_left line 19
  5. lemma OAI.CriticalPercolation.EllipseLinear.center_right line 23
  6. lemma OAI.CriticalPercolation.EllipseLinear.det_lower_of_separation line 27
  7. lemma OAI.CriticalPercolation.EllipseLinear.row_bound line 50
  8. lemma OAI.CriticalPercolation.EllipseLinear.time_sub line 79
  9. lemma OAI.CriticalPercolation.EllipseLinear.height_sub line 82
  10. def OAI.CriticalPercolation.EllipseLinear.equiv line 86
  11. lemma OAI.CriticalPercolation.EllipseLinear.source_budgets line 96