OAI/Probability/SLE/Geometry/RestartConformalRadius.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact composition of the actual restarted maps, obtained from reverse Loewner uniqueness. The conformal-radius and marked-angle identities then use differentiation on the actual surviving domain.

  1. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.restart_inverse_composition line 15
  2. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.restart_forward_composition line 35
  3. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.restart_derivative_composition line 50
  4. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.restart_radius_composition line 73
  5. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.restart_centered_value line 95