OAI/Probability/SLE/SwallowLyapunov.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Swallow Lyapunov for chordal SLE.

  1. def OAI.SLEExactGauge.radialLogPower line 17
  2. def OAI.SLEExactGauge.heightLogPower line 19
  3. def OAI.SLEExactGauge.swallowLyapunov line 20
  4. lemma OAI.SLEExactGauge.radialLogPower_contDiff line 23
  5. lemma OAI.SLEExactGauge.heightLogPower_contDiff line 33
  6. lemma OAI.SLEExactGauge.swallowLyapunov_contDiff line 37
  7. lemma OAI.SLEExactGauge.radialLogPower_directional line 41
  8. lemma OAI.SLEExactGauge.radialLogPower_spatial_deriv line 76
  9. lemma OAI.SLEExactGauge.radialLogPower_spatial_second line 88
  10. lemma OAI.SLEExactGauge.radialLogPower_generator line 118
  11. lemma OAI.SLEExactGauge.heightLogPower_directional line 140
  12. def OAI.SLEExactGauge.swallowGenerator line 161
  13. lemma OAI.SLEExactGauge.swallowLyapunov_generator line 166
  14. lemma OAI.SLEExactGauge.radialLogPower_pos line 199
  15. lemma OAI.SLEExactGauge.heightLogPower_pos line 201
  16. lemma OAI.SLEExactGauge.height_radial_ratio line 206
  17. lemma OAI.SLEExactGauge.swallowGenerator_negative line 222
  18. structure OAI.SLEExactGauge.RadialLocalization line 252
  19. lemma OAI.SLEExactGauge.greenLogNormSq_continuous line 266
  20. lemma OAI.SLEExactGauge.exists_radialLocalization line 271
  21. lemma OAI.SLEExactGauge.RadialLocalization.height_le_initial line 314
  22. lemma OAI.SLEExactGauge.RadialLocalization.chart_identification line 330
  23. lemma OAI.SLEExactGauge.radialLogPower_le line 355
  24. lemma OAI.SLEExactGauge.heightLogPower_le line 365
  25. lemma OAI.SLEExactGauge.radialLogPower_div_lower line 378
  26. lemma OAI.SLEExactGauge.swallowGenerator_uniform_negative line 395
  27. lemma OAI.SLEExactGauge.norm_driver_of_radial_bound line 413
  28. lemma OAI.SLEExactGauge.swallowLyapunov_nonneg line 430
  29. lemma OAI.SLEExactGauge.radialLogPower_at_boundary line 434
  30. lemma OAI.SLEExactGauge.continuous_swallowGenerator line 443
  31. lemma OAI.SLEExactGauge.swallowLyapunov_pair_directional line 468
  32. lemma OAI.SLEExactGauge.exists_compact_swallow_field line 480
  33. lemma OAI.SLEExactGauge.bounded_cumulative_grid_error line 517
  34. theorem OAI.SLEExactGauge.brownian_time_field_stopped_dynkin line 539
  35. lemma OAI.SLEExactGauge.compact_swallow_drift line 628
  36. theorem OAI.SLEExactGauge.ClippedLogSolution.stopped_swallow_dynkin line 646