OAI/Probability/SLE/AngularMoments.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Angular Moments for chordal SLE.

  1. def OAI.SLEExactGauge.physicalGreenLimit line 17
  2. lemma OAI.SLEExactGauge.physicalWeight_exists_limit line 21
  3. lemma OAI.SLEExactGauge.physicalWeight_tendsto_limit line 57
  4. lemma OAI.SLEExactGauge.physicalGreenLimit_bound line 65
  5. lemma OAI.SLEExactGauge.physicalGreenLimit_adapted line 75
  6. lemma OAI.SLEExactGauge.physicalGreenLimit_integrable line 84
  7. theorem OAI.SLEExactGauge.physicalGreenLimit_martingale line 98
  8. def OAI.SLEExactGauge.physicalStoppedGreen line 144
  9. lemma OAI.SLEExactGauge.physicalWeight_tendsto_source line 153
  10. lemma OAI.SLEExactGauge.physicalGreenLimit_eq_source line 219
  11. def OAI.SLEExactGauge.terminalGreenLimit line 243
  12. lemma OAI.SLEExactGauge.localization_weight_tendsto_limit line 247
  13. lemma OAI.SLEExactGauge.terminalGreenLimit_bound line 274
  14. lemma OAI.SLEExactGauge.terminalGreenLimit_stronglyMeasurable line 283
  15. lemma OAI.SLEExactGauge.terminalGreenLimit_integrable line 295
  16. theorem OAI.SLEExactGauge.physicalGreenLimit_condExp_terminal line 308
  17. def OAI.SLEExactGauge.naturalNatFiltration line 371
  18. lemma OAI.SLEExactGauge.terminalGreenLimit_measurable_at_infinity line 376
  19. theorem OAI.SLEExactGauge.physicalGreenLimit_tendsto_at_infinity line 392
  20. lemma OAI.SLEExactGauge.terminalGreenLimit_eq_source line 412
  21. theorem OAI.SLEExactGauge.killedGreen_tendsto_zero_of_no_radius line 424
  22. theorem OAI.SLEExactGauge.exists_physical_green_martingale_regular line 461
  23. lemma OAI.SLEExactGauge.AngularLocalization.physicalWeight_continuous line 526
  24. lemma OAI.SLEExactGauge.AngularLocalization.physicalWeight_stopping_measurable line 534
  25. lemma OAI.SLEExactGauge.AngularLocalization.physicalWeight_stopping_integrable line 544
  26. lemma OAI.SLEExactGauge.AngularLocalization.integral_physicalWeight_stopping line 560
  27. lemma OAI.SLEExactGauge.AngularLocalization.physicalWeight_setIntegral_stopping line 582
  28. lemma OAI.SLEExactGauge.physicalGreenLimit_stopping_measurable line 631
  29. lemma OAI.SLEExactGauge.physicalGreenLimit_stopping_integrable line 644