OAI/Probability/CriticalPercolation/Gluing/CorridorNormalization.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.Corridor.timeCenter line 18
  2. def OAI.CriticalPercolation.Corridor.heightCenter line 19
  3. def OAI.CriticalPercolation.Corridor.normalized line 20
  4. def OAI.CriticalPercolation.Corridor.localTime line 21
  5. def OAI.CriticalPercolation.Corridor.localHeight line 22
  6. def OAI.CriticalPercolation.Corridor.sign line 23
  7. def OAI.CriticalPercolation.Corridor.mark line 25
  8. lemma OAI.CriticalPercolation.Corridor.sign_abs line 28
  9. lemma OAI.CriticalPercolation.Corridor.timeCenter_target line 30
  10. lemma OAI.CriticalPercolation.Corridor.heightCenter_target line 34
  11. lemma OAI.CriticalPercolation.Corridor.normalized_box line 38
  12. lemma OAI.CriticalPercolation.Corridor.normalized_tube line 54
  13. lemma OAI.CriticalPercolation.Corridor.normalized_domain line 85
  14. lemma OAI.CriticalPercolation.Corridor.mark_initial line 96
  15. lemma OAI.CriticalPercolation.Corridor.mark_target line 101
  16. lemma OAI.CriticalPercolation.Corridor.mark_subset_box line 113
  17. lemma OAI.CriticalPercolation.Corridor.coordinateMove_translate line 119