OAI/Probability/SLE/Geometry/NormalizedLoewnerCharts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual inverse/forward capacity charts after translating the driver to zero and applying the positive waypoint dilation. These supply all analytic chart hypotheses in the joint guide compactness argument.

  1. def OAI.SLEExactGauge.normalizedForward line 15
  2. def OAI.SLEExactGauge.normalizedInverse line 18
  3. theorem OAI.SLEExactGauge.normalized_capacity_charts line 21