OAI/Probability/SLELocalization/MappedExit.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Swallowing estimates.

  1. lemma OAI.SLEExactGauge.Swallowing.cutoff_eq_until line 21
  2. def OAI.SLEExactGauge.Swallowing.physicalQ line 49
  3. def OAI.SLEExactGauge.Swallowing.physicalPhi line 53
  4. lemma OAI.SLEExactGauge.Swallowing.budget_dominates line 57
  5. lemma OAI.SLEExactGauge.Swallowing.radial_occupation_point line 127
  6. lemma OAI.SLEExactGauge.Swallowing.occupation_lower line 140
  7. lemma OAI.SLEExactGauge.Swallowing.average_riemann_tendsto line 160
  8. def OAI.SLEExactGauge.Swallowing.heightCut line 183
  9. lemma OAI.SLEExactGauge.Swallowing.heightCut_pos line 185
  10. lemma OAI.SLEExactGauge.Swallowing.heightCut_le line 188
  11. lemma OAI.SLEExactGauge.Swallowing.heightCut_tendsto line 193
  12. def OAI.SLEExactGauge.Swallowing.averagedBudget line 198
  13. lemma OAI.SLEExactGauge.Swallowing.averagedBudget_mean line 205
  14. lemma OAI.SLEExactGauge.Swallowing.budget_terminal_bound line 250
  15. lemma OAI.SLEExactGauge.Swallowing.physical_continuous line 272
  16. lemma OAI.SLEExactGauge.Swallowing.averagedBudget_lower line 291
  17. lemma OAI.SLEExactGauge.Swallowing.eventually_budget_large line 328
  18. lemma OAI.SLEExactGauge.Swallowing.initial_uniform line 367
  19. lemma OAI.SLEExactGauge.Swallowing.survival_bound line 379
  20. theorem OAI.SLEExactGauge.swallowingTime_tail line 428
  21. def OAI.SLEExactGauge.excursionBeforeSwallowing line 464
  22. lemma OAI.SLEExactGauge.Swallowing.early_excursion_forces_driver line 481
  23. lemma OAI.SLEExactGauge.Swallowing.excursion_split line 508
  24. theorem OAI.SLEExactGauge.swallowing_excursion_tail line 552
  25. def OAI.SLEExactGauge.mappedLiveExit line 615
  26. lemma OAI.SLEExactGauge.mappedLiveExit_split line 620
  27. theorem OAI.SLEExactGauge.mapped_live_exit_tail line 630