OAI/Probability/SLE/Gauge/SerpentineFittedChart.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The concrete normalized chart, with the universal local constants used by the ribbon iteration. The physical width is recorded separately.

  1. def OAI.SLEExactGauge.Serpentine.fitSpine line 17
  2. def OAI.SLEExactGauge.Serpentine.fitTangent line 20
  3. def OAI.SLEExactGauge.Serpentine.fitChart line 23
  4. def OAI.SLEExactGauge.Serpentine.positiveCenter line 26
  5. lemma OAI.SLEExactGauge.Serpentine.fitChart_continuous line 29
  6. lemma OAI.SLEExactGauge.Serpentine.fitChart_injective line 34
  7. lemma OAI.SLEExactGauge.Serpentine.fitChart_patch_bounds line 39
  8. lemma OAI.SLEExactGauge.Serpentine.fitChart_upper line 47
  9. lemma OAI.SLEExactGauge.Serpentine.fitChart_initial line 55
  10. lemma OAI.SLEExactGauge.Serpentine.fitChart_width line 69
  11. lemma OAI.SLEExactGauge.Serpentine.fitSpine_eventually_ray line 73
  12. lemma OAI.SLEExactGauge.Serpentine.fit_scaled_arrayCenter line 78