OAI/Probability/SLE/Gauge/SerpentineExperimentGeometry.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The actual left-or-right displaced serpentine. Reflection is applied to both the physical image and the normal coordinate, so the initial chart is still z ↦ I*z.

  1. def OAI.SLEExactGauge.Serpentine.experimentChart line 18
  2. def OAI.SLEExactGauge.Serpentine.experimentSpine line 21
  3. def OAI.SLEExactGauge.Serpentine.physicalExperimentChart line 24
  4. lemma OAI.SLEExactGauge.Serpentine.loewnerMirror_real_mul line 27
  5. lemma OAI.SLEExactGauge.Serpentine.physicalExperimentChart_eq line 31
  6. theorem OAI.SLEExactGauge.Serpentine.experimentChart_geometry line 38
  7. lemma OAI.SLEExactGauge.Serpentine.experimentChart_width line 61
  8. lemma OAI.SLEExactGauge.Serpentine.experimentSpine_eventually_ray line 69
  9. lemma OAI.SLEExactGauge.Serpentine.experimentChart_real_norm line 80
  10. theorem OAI.SLEExactGauge.Serpentine.experimentChart_escape line 85
  11. theorem OAI.SLEExactGauge.Serpentine.experimentChart_zero line 91
  12. theorem OAI.SLEExactGauge.Serpentine.experimentChart_closedEmbedding line 97
  13. theorem OAI.SLEExactGauge.Serpentine.experimentChart_global_progress line 105
  14. lemma OAI.SLEExactGauge.Serpentine.reflected_positiveCenter line 110
  15. theorem OAI.SLEExactGauge.Serpentine.physicalExperimentChart_retained_disk line 124
  16. theorem OAI.SLEExactGauge.Serpentine.physicalExperimentChart_avoids_shadow line 145
  17. theorem OAI.SLEExactGauge.Serpentine.selected_middle_regions_inside line 163