OAI/Probability/SLE/Gauge/SerpentineFittedShadow.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The complete fitted ribbon avoids a fixed upward shadow of the marked point, including the connector and the infinite final tail.

  1. lemma OAI.SLEExactGauge.Serpentine.fit_width_le line 13
  2. lemma OAI.SLEExactGauge.Serpentine.fit_scaledX line 20
  3. lemma OAI.SLEExactGauge.Serpentine.physicalFitChart_low line 25
  4. lemma OAI.SLEExactGauge.Serpentine.physicalFitChart_tail_right line 47
  5. lemma OAI.SLEExactGauge.Serpentine.physicalFitChart_array_right line 65
  6. theorem OAI.SLEExactGauge.Serpentine.physicalFitChart_avoids_shadow line 88