OAI/Probability/SLE/Gauge/SerpentineReflection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Reflecting the deterministic ribbon to the left of the imaginary axis preserves its chart geometry. No stochastic symmetry is used.

  1. def OAI.SLEExactGauge.Serpentine.reflectedChart line 16
  2. lemma OAI.SLEExactGauge.Serpentine.conj_mem_closedRibbon line 18
  3. lemma OAI.SLEExactGauge.Serpentine.conj_mem_stepPatch line 21
  4. lemma OAI.SLEExactGauge.Serpentine.reflectedChart_continuous line 25
  5. lemma OAI.SLEExactGauge.Serpentine.reflectedChart_injective line 28
  6. lemma OAI.SLEExactGauge.Serpentine.reflectedChart_patch_upper line 34
  7. lemma OAI.SLEExactGauge.Serpentine.reflectedChart_patch_lower line 42
  8. lemma OAI.SLEExactGauge.Serpentine.reflectedChart_upper line 50
  9. lemma OAI.SLEExactGauge.Serpentine.reflectedChart_initial line 57
  10. lemma OAI.SLEExactGauge.Serpentine.reflectedChart_width line 64