OAI/Probability/SLE/Loewner/RawInverseDriverApproximation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A geometric inverse witness approaches the raw inverse under a uniform driver perturbation. The reference driver needs no trace.

  1. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.raw_inverse_driver_distance line 14
  2. theorem OAI.SLEExactGauge.raw_inverse_limit_of_witness_drivers line 33