OAI/Probability/SLELocalization/BrownianSupport.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Brownian Support estimates.

  1. lemma OAI.SLEExactGauge.BrownianSupport.preBrownian_past_square_le line 16
  2. lemma OAI.SLEExactGauge.BrownianSupport.preBrownian_square_submartingale line 68
  3. lemma OAI.SLEExactGauge.BrownianSupport.preBrownian_finite_max_bound line 85
  4. def OAI.SLEExactGauge.BrownianPredictable.restartIndex line 129
  5. def OAI.SLEExactGauge.BrownianPredictable.restartGrid line 132
  6. def OAI.SLEExactGauge.BrownianPredictable.restartTime line 134
  7. lemma OAI.SLEExactGauge.BrownianPredictable.restartIndex_aemeasurable line 137
  8. lemma OAI.SLEExactGauge.BrownianPredictable.restartTime_bounds line 141
  9. lemma OAI.SLEExactGauge.BrownianPredictable.restartTime_tendsto line 154
  10. lemma OAI.SLEExactGauge.BrownianPredictable.restartIndex_past line 162
  11. lemma OAI.SLEExactGauge.BrownianSupport.brownian_finite_max_bound line 215
  12. lemma OAI.SLEExactGauge.BrownianSupport.brownian_oscillation_bound line 233
  13. def OAI.SLEExactGauge.BrownianSupport.densityFloor line 289
  14. lemma OAI.SLEExactGauge.BrownianSupport.densityFloor_pos line 291
  15. lemma OAI.SLEExactGauge.BrownianSupport.gaussian_pdf_lower line 295
  16. lemma OAI.SLEExactGauge.BrownianSupport.gaussian_short_interval_lower line 315
  17. lemma OAI.SLEExactGauge.BrownianSupport.short_endpoint_dominates line 349
  18. def OAI.SLEExactGauge.BrownianSupport.probeTime line 386
  19. lemma OAI.SLEExactGauge.BrownianSupport.probeTime_le line 388
  20. lemma OAI.SLEExactGauge.BrownianSupport.continuous_probeTime line 392
  21. def OAI.SLEExactGauge.BrownianSupport.stepSet line 396
  22. lemma OAI.SLEExactGauge.BrownianSupport.measurableSet_stepSet line 399
  23. lemma OAI.SLEExactGauge.BrownianSupport.probe_bound_all line 407
  24. def OAI.SLEExactGauge.BrownianSupport.stepEvent line 429
  25. lemma OAI.SLEExactGauge.BrownianSupport.stepEvent_past line 432
  26. lemma OAI.SLEExactGauge.BrownianSupport.small_step_pos line 449
  27. lemma OAI.SLEExactGauge.BrownianSupport.past_inter_step line 482
  28. def OAI.SLEExactGauge.BrownianSupport.stepsEvent line 490
  29. lemma OAI.SLEExactGauge.BrownianSupport.stepsEvent_zero line 494
  30. lemma OAI.SLEExactGauge.BrownianSupport.stepsEvent_succ line 499
  31. lemma OAI.SLEExactGauge.BrownianSupport.stepsEvent_past line 507
  32. lemma OAI.SLEExactGauge.BrownianSupport.stepsEvent_pos line 519
  33. lemma OAI.SLEExactGauge.BrownianSupport.exists_grid_interval line 530
  34. lemma OAI.SLEExactGauge.BrownianSupport.endpoint_error_bound line 544
  35. lemma OAI.SLEExactGauge.BrownianSupport.tube_of_steps line 565
  36. lemma OAI.SLEExactGauge.BrownianSupport.lipschitzTube_pos line 615
  37. theorem OAI.SLEExactGauge.BrownianSupport.uniformTube_pos line 686