OAI/Probability/SLELocalization/EuclideanApproach.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Is Loewner Trace Using estimates.

  1. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.visit_liveDistanceApproach line 17
  2. lemma OAI.SLEExactGauge.SmallTarget.sqrt_rpow line 93
  3. lemma OAI.SLEExactGauge.SmallTarget.interior_weight line 98
  4. lemma OAI.SLEExactGauge.SmallTarget.interior_power_product line 113
  5. lemma OAI.SLEExactGauge.SmallTarget.radius_power line 120
  6. theorem OAI.SLEExactGauge.SmallTarget.interior_trace_bound line 124
  7. lemma OAI.SLEExactGauge.SmallTarget.epsilon_le_sqrt line 170
  8. lemma OAI.SLEExactGauge.SmallTarget.near_real_geometry line 175
  9. lemma OAI.SLEExactGauge.SmallTarget.cutoff_sqrt_small line 196
  10. theorem OAI.SLEExactGauge.uniform_small_target line 216
  11. lemma OAI.SLEExactGauge.SmallTarget.scaled_near_real_geometry line 314
  12. lemma OAI.SLEExactGauge.SmallTarget.scaled_interior_power line 337
  13. theorem OAI.SLEExactGauge.SmallTarget.interior_trace_scaled_bound line 345
  14. lemma OAI.SLEExactGauge.scaled_annulus_real_bound line 402
  15. theorem OAI.SLEExactGauge.uniform_small_target_scaled line 421
  16. def OAI.SLEExactGauge.RectangleEnergy.logTrace line 523
  17. lemma OAI.SLEExactGauge.RectangleEnergy.dyadic_radius_power line 526
  18. theorem OAI.SLEExactGauge.RectangleEnergy.logTrace_dyadic_hitting line 532
  19. instance OAI.SLEExactGauge.RectangleEnergy.DRect.(instance at line 593) line 593
  20. lemma OAI.SLEExactGauge.RectangleEnergy.DRect.measure_subset line 595
  21. lemma OAI.SLEExactGauge.RectangleEnergy.DRect.child_measure_le line 600
  22. lemma OAI.SLEExactGauge.RectangleEnergy.DRect.measure_interval_split line 604
  23. lemma OAI.SLEExactGauge.RectangleEnergy.DRect.measure_child_sum line 611
  24. lemma OAI.SLEExactGauge.RectangleEnergy.dyadicRect_measure_le line 631
  25. lemma OAI.SLEExactGauge.RectangleEnergy.dyadic_measure_sum line 636
  26. lemma OAI.SLEExactGauge.RectangleEnergy.dyadic_integral_sum line 649
  27. def OAI.SLEExactGauge.RectangleEnergy.jumpSize line 667
  28. lemma OAI.SLEExactGauge.RectangleEnergy.jumpSize_pos line 669
  29. lemma OAI.SLEExactGauge.RectangleEnergy.jumpSize_telescope line 673
  30. lemma OAI.SLEExactGauge.RectangleEnergy.exists_large_increment line 681
  31. lemma OAI.SLEExactGauge.RectangleEnergy.geometric_moment_summable line 703
  32. lemma OAI.SLEExactGauge.RectangleEnergy.branch_bad_parent line 734
  33. lemma OAI.SLEExactGauge.RectangleEnergy.jump_energy_scale line 769
  34. theorem OAI.SLEExactGauge.RectangleEnergy.dyadic_energy_hitting line 777
  35. theorem OAI.SLEExactGauge.RectangleEnergy.strip_rectangle_hitting_discrete line 857
  36. lemma OAI.SLEExactGauge.RectangleEnergy.geometric_floor_bound line 908
  37. lemma OAI.SLEExactGauge.RectangleEnergy.critical_floor line 915
  38. theorem OAI.SLEExactGauge.RectangleEnergy.strip_rectangle_hitting line 922
  39. def OAI.SLEExactGauge.RectangleEnergy.localizationMeanConstant line 972
  40. lemma OAI.SLEExactGauge.RectangleEnergy.localizationMeanConstant_pos line 974
  41. def OAI.SLEExactGauge.RectangleEnergy.localizationStripWidth line 978
  42. lemma OAI.SLEExactGauge.RectangleEnergy.localizationStripWidth_pos line 980