OAI/Probability/SLE/Stochastic/PlanarWienerMoments.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

First-moment control of the actual two-coordinate Wiener increments.

  1. lemma OAI.SLEExactGauge.planarWiener_increment_integrable line 16
  2. lemma OAI.SLEExactGauge.planarWiener_increment_norm_mean line 24
  3. lemma OAI.SLEExactGauge.planarWiener_continuous line 53
  4. lemma OAI.SLEExactGauge.planarWiener_joint_measurable line 56