OAI/Probability/SLE/Loewner/CapacityLoewnerIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The right Loewner evolution has a continuous kernel. Its integral identity therefore gives the ordinary derivative on the full prefix.

  1. theorem OAI.SLEExactGauge.capacityForward_integral_kernel line 14
  2. theorem OAI.SLEExactGauge.capacityForward_hasDerivWithinAt_prefix line 29