OAI/Probability/SLE/Loewner/CapacityLoewnerDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

At every differentiability point the real time derivative is the identified Loewner kernel. Lipschitz regularity then gives the a.e. ODE.

  1. theorem OAI.SLEExactGauge.capacityForward_deriv_at_capacity line 15
  2. lemma OAI.SLEExactGauge.capacityParameterOnPrefix_le line 38
  3. def OAI.SLEExactGauge.capacityDriverOnPrefix line 43
  4. theorem OAI.SLEExactGauge.capacityForward_ae_loewner line 49