OAI/Probability/CriticalPercolation/Gluing/RelayGeometry.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.Relay.width line 13
  2. def OAI.CriticalPercolation.Relay.selectedSign line 14
  3. def OAI.CriticalPercolation.Relay.domain line 16
  4. lemma OAI.CriticalPercolation.Relay.width_lower line 21
  5. lemma OAI.CriticalPercolation.Relay.width_upper line 22
  6. lemma OAI.CriticalPercolation.Relay.width_next line 25
  7. lemma OAI.CriticalPercolation.Relay.width_last line 31
  8. lemma OAI.CriticalPercolation.Relay.selectedSign_cases line 36
  9. lemma OAI.CriticalPercolation.Relay.selectedSign_abs line 40
  10. lemma OAI.CriticalPercolation.Relay.move_towards_axis line 43
  11. lemma OAI.CriticalPercolation.Relay.full_step_height line 51
  12. lemma OAI.CriticalPercolation.Relay.full_step_time line 69
  13. lemma OAI.CriticalPercolation.Relay.path_axis_bound line 76
  14. lemma OAI.CriticalPercolation.Relay.band_mem_domain line 98
  15. lemma OAI.CriticalPercolation.Relay.move_path_contained line 125
  16. lemma OAI.CriticalPercolation.Relay.last_crossing_height line 140
  17. lemma OAI.SimpleGraph.Walk.exists_first_crossing line 159