OAI/Probability/SLELocalization/PhysicalPast.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Conformal localization and Physical Past estimates.

  1. def OAI.SLEExactGauge.PhysicalPast.sampleTime line 19
  2. lemma OAI.SLEExactGauge.PhysicalPast.sampleTime_le line 21
  3. lemma OAI.SLEExactGauge.PhysicalPast.uniform_margin_iff line 25
  4. def OAI.SLEExactGauge.PhysicalPast.avoids line 42
  5. lemma OAI.SLEExactGauge.PhysicalPast.avoids_measurable_past line 47
  6. lemma OAI.SLEExactGauge.PhysicalPast.avoids_nullMeasurable line 60
  7. lemma OAI.SLEExactGauge.PhysicalPast.avoids_eq_source line 71
  8. lemma OAI.SLEExactGauge.closedBall_subset_survivingDomain line 116
  9. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.radius_ge_half_free_ball line 141
  10. def OAI.SLEExactGauge.firstLiveDistanceStop line 199
  11. def OAI.SLEExactGauge.physicalStoppedDensity line 203
  12. lemma OAI.SLEExactGauge.PhysicalStop.le_of_hit line 224
  13. lemma OAI.SLEExactGauge.PhysicalStop.eq_top_iff line 228
  14. lemma OAI.SLEExactGauge.PhysicalStop.finite_spec line 241
  15. lemma OAI.SLEExactGauge.PhysicalStop.lt_stop_distance line 271
  16. lemma OAI.SLEExactGauge.PhysicalStop.stopped_survival_iff line 276
  17. lemma OAI.SLEExactGauge.PhysicalStop.finite_dist_eq line 292
  18. lemma OAI.SLEExactGauge.PhysicalStop.trace_distance_ge_before line 307
  19. lemma OAI.SLEExactGauge.IsLoewnerTraceUsing.radius_ge_before_distance_stop line 336
  20. def OAI.SLEExactGauge.PhysicalStop.cap line 376
  21. lemma OAI.SLEExactGauge.PhysicalStop.cap_bounds line 378
  22. lemma OAI.SLEExactGauge.PhysicalStop.lt_cap line 384
  23. lemma OAI.SLEExactGauge.PhysicalStop.cap_coe line 393
  24. lemma OAI.SLEExactGauge.BrownianField.FieldRegular.restrict line 408
  25. lemma OAI.SLEExactGauge.LoewnerLocalized.integral_drift_cancel_before line 429
  26. def OAI.SLEExactGauge.FiniteTilt.Cutoff.physicalTime line 463
  27. def OAI.SLEExactGauge.FiniteTilt.Cutoff.physicalValue line 466
  28. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.physicalTime_bounds line 470
  29. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.physicalValue_nonneg line 474
  30. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.physicalValue_bound line 477
  31. def OAI.SLEExactGauge.FiniteTilt.Cutoff.physicalCoeff line 493
  32. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.physicalCoeff_measurable_past line 500
  33. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.physicalCoeff_aemeasurable line 507
  34. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.physicalCoeff_eq line 515
  35. theorem OAI.SLEExactGauge.FiniteTilt.Cutoff.physical_centered line 554
  36. theorem OAI.SLEExactGauge.FiniteTilt.Cutoff.physical_expectation line 641
  37. theorem OAI.SLEExactGauge.FiniteTilt.Cutoff.physical_sum_tendsto line 687
  38. lemma OAI.SLEExactGauge.BrownianPredictable.delayed_indicator_difference_centered line 798
  39. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.physical_avoidance_setIntegral line 873
  40. lemma OAI.SLEExactGauge.FiniteTilt.Cutoff.physicalValue_eq_source line 962
  41. lemma OAI.SLEExactGauge.FiniteTilt.eventually_physicalValue_at_hit line 1002
  42. lemma OAI.SLEExactGauge.FiniteTilt.tendsto_physicalValue_killed line 1031