OAI/Probability/SLE/Stochastic/PlanarDynkin.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Dynkin's formula for compact smooth tests of the actual planar Wiener path, relative to its full two-coordinate past.

  1. lemma OAI.SLEExactGauge.planar_compact_eval_integrable line 15
  2. lemma OAI.SLEExactGauge.planar_generator_joint_measurable line 25
  3. theorem OAI.SLEExactGauge.planarWiener_dynkin line 31