OAI/Probability/SLE/StoppedPower.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Stopped Power for chordal SLE.

  1. def OAI.SLEExactGauge.powerLogGenerator line 15
  2. lemma OAI.SLEExactGauge.continuous_powerLogGenerator line 21
  3. lemma OAI.SLEExactGauge.measurable_powerLogGenerator_comp line 32
  4. lemma OAI.SLEExactGauge.compact_power_drift line 40
  5. theorem OAI.SLEExactGauge.ClippedLogSolution.stopped_power_dynkin line 58
  6. lemma OAI.SLEExactGauge.stopping_paste_after line 160
  7. theorem OAI.SLEExactGauge.ClippedLogSolution.stopped_green_bounded_clock line 184
  8. theorem OAI.SLEExactGauge.ClippedLogSolution.stopped_green_history line 285
  9. lemma OAI.SLEExactGauge.exists_brownian_compact_stops line 341
  10. lemma OAI.SLEExactGauge.bounded_stopped_cumulative_integrable line 396
  11. lemma OAI.SLEExactGauge.integral_tendsto_stopped_eval line 416
  12. lemma OAI.SLEExactGauge.integral_identity_of_stable_stops line 429
  13. lemma OAI.SLEExactGauge.ClippedLogSolution.stopped_power_dynkin_compact_cap line 454
  14. lemma OAI.SLEExactGauge.ClippedLogSolution.stopped_power_integrable line 481
  15. lemma OAI.SLEExactGauge.ClippedLogSolution.power_generator_measurable line 496
  16. lemma OAI.SLEExactGauge.ClippedLogSolution.stopped_power_cumulative_integrable line 511
  17. theorem OAI.SLEExactGauge.ClippedLogSolution.stopped_power_dynkin_bounded line 533
  18. lemma OAI.SLEExactGauge.ClippedLogSolution.swallow_generator_measurable line 596
  19. lemma OAI.SLEExactGauge.ClippedLogSolution.swallow_generator_continuous line 608
  20. lemma OAI.SLEExactGauge.ClippedLogSolution.swallow_cumulative_integrable line 620
  21. lemma OAI.SLEExactGauge.bounded_nnreal_integrable line 637
  22. lemma OAI.SLEExactGauge.RadialLocalization.exists_compact_bound line 661
  23. lemma OAI.SLEExactGauge.RadialLocalization.exists_generator_bound line 672
  24. lemma OAI.SLEExactGauge.RadialLocalization.generator_cumulative_integrable line 685
  25. lemma OAI.SLEExactGauge.RadialLocalization.stopped_lyapunov_bound line 695
  26. theorem OAI.SLEExactGauge.compensated_exponential_limit line 752
  27. theorem OAI.SLEExactGauge.compensated_exponential_limit_energy line 781
  28. theorem OAI.SLEExactGauge.exponential_tail_of_compensated line 804
  29. theorem OAI.SLEExactGauge.subGaussian_tail_of_compensated line 829