OAI/Probability/SLE/FiniteRadiusStop.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Finite Radius Stop for chordal SLE.

  1. lemma OAI.SLEExactGauge.continuous_nonneg_at_boundary line 17
  2. theorem OAI.SLEExactGauge.first_margin_stopping line 32
  3. def OAI.SLEExactGauge.logStopMargin line 61
  4. lemma OAI.SLEExactGauge.continuous_logStopMargin line 66
  5. lemma OAI.SLEExactGauge.logStopMargin_nonneg_iff line 75
  6. lemma OAI.SLEExactGauge.logStopMargin_pos_iff line 81
  7. lemma OAI.SLEExactGauge.ClippedLogSolution.norm_le line 87
  8. theorem OAI.SLEExactGauge.ClippedLogSolution.finite_radius_cutoff line 103
  9. lemma OAI.SLEExactGauge.continuous_path_bounded_by_nat line 226
  10. lemma OAI.SLEExactGauge.first_radius_angle_le line 234
  11. lemma OAI.SLEExactGauge.bounded_iSup_stopping line 243
  12. lemma OAI.SLEExactGauge.greenLogDensity_nonneg line 258
  13. lemma OAI.SLEExactGauge.greenLogDensity_le_radius line 261
  14. theorem OAI.SLEExactGauge.ClippedLogSolution.finite_angular_law line 270
  15. def OAI.SLEExactGauge.initialLogCoordinates line 392
  16. def OAI.SLEExactGauge.restoreLogPoint line 395
  17. lemma OAI.SLEExactGauge.restoreLogPoint_im line 398
  18. lemma OAI.SLEExactGauge.restoreLogPoint_initial line 402
  19. lemma OAI.SLEExactGauge.restoreLogPoint_derivative line 406
  20. theorem OAI.SLEExactGauge.clipped_log_identification line 439
  21. theorem OAI.SLEExactGauge.exists_joint_clipped_flow line 485
  22. lemma OAI.SLEExactGauge.measurable_initialLogCoordinates line 524
  23. theorem OAI.SLEExactGauge.exists_spatial_clipped_flow line 530
  24. lemma OAI.SLEExactGauge.clipped_log_height_derivative line 557
  25. lemma OAI.SLEExactGauge.clipped_log_height_antitone line 569
  26. lemma OAI.SLEExactGauge.clipped_log_identification_of_endpoint line 584
  27. def OAI.SLEExactGauge.powerLogDensity line 616
  28. lemma OAI.SLEExactGauge.powerLogDensity_contDiff line 620
  29. lemma OAI.SLEExactGauge.powerLogDensity_spatial_derivative line 635
  30. lemma OAI.SLEExactGauge.powerLogDensity_spatial_second line 652
  31. lemma OAI.SLEExactGauge.powerLogDensity_directional line 684
  32. lemma OAI.SLEExactGauge.powerLogDensity_pair_directional line 727
  33. lemma OAI.SLEExactGauge.exists_compact_power_field line 739
  34. lemma OAI.SLEExactGauge.power_physical_generator line 767
  35. lemma OAI.SLEExactGauge.powerLogDensity_radius_angle line 784
  36. lemma OAI.SLEExactGauge.green_weighted_power_generator line 797