OAI/Probability/SLE/ExponentialMartingales.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Exponential Martingales for chordal SLE.

  1. lemma OAI.SLEExactGauge.finite_uniformIntegrable_one_of_eLpNorm_two_bounded line 55
  2. theorem OAI.SLEExactGauge.finite_L1_tendsto_of_square_bound line 103
  3. lemma OAI.SLEExactGauge.product_memLp_two_of_section_square_bound line 129
  4. lemma OAI.SLEExactGauge.area_eLpNorm_one_le_product line 153
  5. theorem OAI.SLEExactGauge.area_L1_tendsto_of_square_bound line 175
  6. lemma OAI.SLEExactGauge.area_driver_sum line 203
  7. theorem OAI.SLEExactGauge.brownian_area_sum_L1_limit line 219
  8. theorem OAI.SLEExactGauge.brownian_area_exponential_limit line 291
  9. def OAI.SLEExactGauge.areaPrefixSample line 353
  10. lemma OAI.SLEExactGauge.areaPrefixSample_measurable line 357
  11. lemma OAI.SLEExactGauge.areaPrefixSample_bound line 363
  12. lemma OAI.SLEExactGauge.prefix_pair_energy_tendsto line 372
  13. lemma OAI.SLEExactGauge.prefix_pair_energy_bound line 390
  14. theorem OAI.SLEExactGauge.area_prefix_energy_tendsto line 413
  15. lemma OAI.SLEExactGauge.interval_integral_prefix_lt line 461
  16. theorem OAI.SLEExactGauge.area_prefix_energy_identity line 475
  17. def OAI.SLEExactGauge.areaWindowSample line 532
  18. lemma OAI.SLEExactGauge.areaWindowSample_measurable line 536
  19. lemma OAI.SLEExactGauge.areaWindowSample_bound line 543
  20. lemma OAI.SLEExactGauge.window_pair_eq_prefix_difference line 552
  21. lemma OAI.SLEExactGauge.window_pair_energy_tendsto line 571
  22. lemma OAI.SLEExactGauge.window_pair_energy_bound line 592
  23. lemma OAI.SLEExactGauge.area_window_pair_energy_tendsto line 613
  24. lemma OAI.SLEExactGauge.real_window_pair_eq line 662
  25. theorem OAI.SLEExactGauge.area_window_energy_identity line 679