OAI/Probability/SLELocalization/LoewnerExit.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Loewner Exit estimates.

  1. lemma OAI.SLEExactGauge.LoewnerExit.stop_le_of_nonpos line 18
  2. lemma OAI.SLEExactGauge.LoewnerExit.stop_prefix_min line 29
  3. def OAI.SLEExactGauge.FiniteTilt.Cutoff.withHorizon line 73
  4. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.withHorizon_gt line 84
  5. def OAI.SLEExactGauge.RadiusPast.hitData line 102
  6. lemma OAI.SLEExactGauge.RadiusPast.measurable_hitData line 108
  7. lemma OAI.SLEExactGauge.RadiusPast.raw_data_source line 139
  8. lemma OAI.SLEExactGauge.RadiusPast.eventually_stop_general line 186
  9. lemma OAI.SLEExactGauge.RadiusPast.live_radius_witness line 219
  10. def OAI.SLEExactGauge.RadiusPast.byTime line 234
  11. def OAI.SLEExactGauge.RadiusPast.approx line 239
  12. lemma OAI.SLEExactGauge.RadiusPast.eventually_approx line 245
  13. def OAI.SLEExactGauge.RadiusPast.observed line 302
  14. lemma OAI.SLEExactGauge.RadiusPast.measurable_observed line 306
  15. lemma OAI.SLEExactGauge.RadiusPast.aemeasurable_observed line 318
  16. lemma OAI.SLEExactGauge.RadiusPast.observed_eq line 330
  17. lemma OAI.SLEExactGauge.RadiusPast.byTime_pos_iff line 346
  18. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.firstLiveRadiusStop_mono line 381
  19. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.firstLiveRadiusStop_pos line 399
  20. def OAI.SLEExactGauge.CompletedStoppedPast line 428
  21. lemma OAI.SLEExactGauge.CompletedStoppedPast.empty line 449
  22. lemma OAI.SLEExactGauge.CompletedStoppedPast.union line 454
  23. lemma OAI.SLEExactGauge.CompletedStoppedPast.diff line 468
  24. lemma OAI.SLEExactGauge.CompletedStoppedPast.mono line 482
  25. lemma OAI.SLEExactGauge.finiteStoppedDensity_stoppedPast line 515
  26. lemma OAI.SLEExactGauge.CompletedStoppedPast.finsetUnion line 572
  27. def OAI.SLEExactGauge.FiniteFirstEvents.first line 598
  28. lemma OAI.SLEExactGauge.FiniteFirstEvents.first_subset line 601
  29. lemma OAI.SLEExactGauge.FiniteFirstEvents.first_disjoint line 604
  30. lemma OAI.SLEExactGauge.FiniteFirstEvents.union_first line 613
  31. lemma OAI.SLEExactGauge.FiniteFirstEvents.first_stoppedPast line 632
  32. lemma OAI.SLEExactGauge.finiteCenteredMeasure_event_le line 657
  33. def OAI.SLEExactGauge.densityBelow line 695
  34. lemma OAI.SLEExactGauge.finiteCentered_grid_le line 699
  35. lemma OAI.SLEExactGauge.finiteCentered_countableGrid_le line 763
  36. def OAI.SLEExactGauge.FiniteClock.angleFloor line 818
  37. def OAI.SLEExactGauge.FiniteClock.threshold line 820
  38. def OAI.SLEExactGauge.FiniteClock.blockThreshold line 823
  39. lemma OAI.SLEExactGauge.FiniteClock.exponent_pos line 827
  40. lemma OAI.SLEExactGauge.FiniteClock.codimension_pos line 831
  41. lemma OAI.SLEExactGauge.FiniteClock.angleFloor_pos line 835
  42. lemma OAI.SLEExactGauge.FiniteClock.threshold_formula line 839
  43. lemma OAI.SLEExactGauge.FiniteClock.threshold_le_block line 852
  44. lemma OAI.SLEExactGauge.FiniteClock.block_cancel line 871
  45. def OAI.SLEExactGauge.FiniteClock.blockIndex line 888
  46. def OAI.SLEExactGauge.FiniteClock.blockBad line 891
  47. lemma OAI.SLEExactGauge.FiniteClock.blockBad_subset_hit line 895
  48. lemma OAI.SLEExactGauge.FiniteClock.ordinary_natural_radius_bound line 915
  49. lemma OAI.SLEExactGauge.FiniteClock.block_bound line 949
  50. def OAI.SLEExactGauge.FiniteClock.bad line 995
  51. lemma OAI.SLEExactGauge.FiniteClock.mem_bad_of_rational line 999
  52. lemma OAI.SLEExactGauge.FiniteClock.geometric_blocks line 1008
  53. lemma OAI.SLEExactGauge.FiniteClock.bad_bound line 1025
  54. lemma OAI.SLEExactGauge.FiniteClock.exists_small_floor line 1044
  55. lemma OAI.SLEExactGauge.FiniteClock.rational_clock_nonneg line 1053