OAI/Probability/SLE/Loewner/FreshCapacityWitness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The published trace-generation input is used only on the single continuous Brownian path law. Strong Markov supplies the fresh witness.

  1. theorem OAI.SLEExactGauge.fresh_capacity_witness_exists line 17