OAI/Probability/SLE/Gauge/GaugeConformalReduction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The explicit gauge needs no independent normal-family input once the disk growth estimate is available.

  1. theorem OAI.SLEExactGauge.ordinary_explicit_mainConclusion_of_boundary_support_crosscut_exit line 16
  2. theorem OAI.SLEExactGauge.ordinary_explicit_mainConclusion_of_geometric_inputs line 28
  3. theorem OAI.SLEExactGauge.ordinary_explicit_mainConclusion_of_growth_and_geometric_inputs line 41