OAI/Probability/SLELocalization/AngularClock.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Gamma Field estimates.

  1. lemma OAI.SLEExactGauge.GammaField.field_nonneg line 21
  2. lemma OAI.SLEExactGauge.GammaField.field_initial line 27
  3. lemma OAI.SLEExactGauge.GammaField.measurable_stop line 37
  4. lemma OAI.SLEExactGauge.GammaField.integral_drift_nonpos line 58
  5. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.remaining_upper line 108
  6. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.ratio_upper line 128
  7. def OAI.SLEExactGauge.GammaField.pathTerminal line 149
  8. lemma OAI.SLEExactGauge.GammaField.continuous_actualField line 154
  9. lemma OAI.SLEExactGauge.GammaField.pathTerminal_measurable line 167
  10. lemma OAI.SLEExactGauge.GammaField.pathTerminal_eq line 180
  11. lemma OAI.SLEExactGauge.GammaField.terminal_aemeasurable line 192
  12. def OAI.SLEExactGauge.FiniteTilt.Cutoff.barrier line 221
  13. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.barrier_nonneg line 225
  14. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.barrier_aemeasurable line 233
  15. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.barrier_expectation line 257
  16. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.barrier_at_radius line 375
  17. lemma OAI.SLEExactGauge.FiniteTilt.eventually_stop_at_radius line 413
  18. def OAI.SLEExactGauge.FiniteTilt.timeShift line 434
  19. lemma OAI.SLEExactGauge.FiniteTilt.timeShift_pos line 437
  20. lemma OAI.SLEExactGauge.FiniteTilt.timeShift_tendsto line 440
  21. lemma OAI.SLEExactGauge.FiniteTilt.barrier_tendsto_on_hit line 448
  22. lemma OAI.SLEExactGauge.radiusApproachProfile line 485
  23. lemma OAI.SLEExactGauge.squaredSine_initial line 538
  24. theorem OAI.SLEExactGauge.radiusApproachBound line 549
  25. lemma OAI.SLEExactGauge.UnivalentDistance.derivative_variation line 595
  26. lemma OAI.SLEExactGauge.UnivalentDistance.local_image_disk line 619
  27. lemma OAI.SLEExactGauge.UnivalentDistance.image_disk line 671
  28. lemma OAI.SLEExactGauge.UnivalentDistance.exp_injective_derivative_bound line 722
  29. lemma OAI.SLEExactGauge.UnivalentDistance.omitted_value_bound line 746
  30. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.radius_le_complement_distance line 793
  31. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.radius_le_boundary_distance line 847
  32. def OAI.SLEExactGauge.liveDistanceApproach line 873
  33. lemma OAI.SLEExactGauge.liveDistanceApproach_radius_hit line 876
  34. theorem OAI.SLEExactGauge.euclideanApproachBound line 895
  35. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.future_tip_mem_closure line 966