OAI/Probability/SLE/DiskHalfPlane.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Disk Half Plane for chordal SLE.

  1. def OAI.SLEExactGauge.diskToHalfPlane line 15
  2. lemma OAI.SLEExactGauge.disk_denominator_ne line 17
  3. lemma OAI.SLEExactGauge.diskToHalfPlane_im line 23
  4. lemma OAI.SLEExactGauge.diskToHalfPlane_maps line 30
  5. lemma OAI.SLEExactGauge.diskToHalfPlane_differentiable line 40
  6. lemma OAI.SLEExactGauge.diskToHalfPlane_zero line 45
  7. lemma OAI.SLEExactGauge.diskToHalfPlane_deriv_zero line 47
  8. lemma OAI.SLEExactGauge.diskToHalfPlane_injOn line 53
  9. lemma OAI.SLEExactGauge.norm_sub_conj_of_im_pos line 64
  10. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.radius_le_omitted_distance line 80
  11. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.radius_le_past_distance line 126
  12. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.radius_approach_of_trace_approach line 147
  13. lemma OAI.SLEExactGauge.logRadiusClock_logCoordinates line 202
  14. lemma OAI.SLEExactGauge.fullRadius_eq_logClock line 218
  15. lemma OAI.SLEExactGauge.fullRadius_level_iff_logClock line 228
  16. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.radius_clock_strictMonoOn line 237
  17. lemma OAI.SLEExactGauge.live_radius_unique line 253
  18. lemma OAI.SLEExactGauge.live_clock_le_time line 269
  19. lemma OAI.SLEExactGauge.live_angleSq_lower_bound line 284
  20. lemma OAI.SLEExactGauge.radiusLevelTime_eq_of_live_level line 312
  21. lemma OAI.SLEExactGauge.stoppedGreen_eq_of_live_level line 332
  22. lemma OAI.SLEExactGauge.stoppedGreen_eq_zero_of_no_level line 341
  23. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.fullRadius_initial line 364
  24. lemma OAI.SLEExactGauge.radiusLevelTime_finite_of_live_radius_lt line 375
  25. structure OAI.SLEExactGauge.FiniteIncreasingClock line 420
  26. lemma OAI.SLEExactGauge.FiniteIncreasingClock.terminal_nonneg line 430
  27. def OAI.SLEExactGauge.FiniteIncreasingClock.iso line 435
  28. lemma OAI.SLEExactGauge.FiniteIncreasingClock.iso_apply line 451
  29. def OAI.SLEExactGauge.FiniteIncreasingClock.inverse line 454
  30. lemma OAI.SLEExactGauge.FiniteIncreasingClock.inverse_mem line 458
  31. lemma OAI.SLEExactGauge.FiniteIncreasingClock.clock_inverse line 461
  32. lemma OAI.SLEExactGauge.FiniteIncreasingClock.inverse_clock line 465
  33. lemma OAI.SLEExactGauge.FiniteIncreasingClock.continuous_inverse line 476
  34. lemma OAI.SLEExactGauge.FiniteIncreasingClock.inverse_le_iff line 481
  35. lemma OAI.SLEExactGauge.FiniteIncreasingClock.measurable_inverse line 490
  36. lemma OAI.SLEExactGauge.powerLogDensity_pos line 525
  37. lemma OAI.SLEExactGauge.powerLogDensity_le_radius line 528
  38. lemma OAI.SLEExactGauge.powerLogGenerator_abs_bound line 541
  39. lemma OAI.SLEExactGauge.powerLogGenerator_le_radius_height line 576
  40. theorem OAI.SLEExactGauge.exists_finite_angular_kernel line 600
  41. structure OAI.SLEExactGauge.AngularLocalization line 691
  42. lemma OAI.SLEExactGauge.initialLogCoordinates_im line 714
  43. lemma OAI.SLEExactGauge.exists_angularLocalization line 718
  44. lemma OAI.SLEExactGauge.AngularLocalization.chart_identification line 756
  45. lemma OAI.SLEExactGauge.AngularLocalization.clock_eq_chart line 771
  46. lemma OAI.SLEExactGauge.AngularLocalization.clock_stopped_measurable line 782
  47. lemma OAI.SLEExactGauge.AngularLocalization.mean_green line 794