OAI/Probability/SLE/Geometry/StoppedMarkedStateMeasurability.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Actual finite-stop marked states are measurable in the stopped past. The scale is positive on every outcome and agrees with the true centered modulus on the live event.

  1. def OAI.SLEExactGauge.positiveMarkedScale line 16
  2. lemma OAI.SLEExactGauge.positiveMarkedScale_pos line 18
  3. lemma OAI.SLEExactGauge.positiveMarkedScale_eq line 24
  4. lemma OAI.SLEExactGauge.positiveMarkedScale_measurable line 27
  5. lemma OAI.SLEExactGauge.unitMarkedState_measurable line 31
  6. def OAI.SLEExactGauge.stoppedMarkedCenter line 35
  7. def OAI.SLEExactGauge.stoppedMarkedScale line 41
  8. def OAI.SLEExactGauge.stoppedMarkedUnit line 45
  9. def OAI.SLEExactGauge.stoppedMarkedGood line 49
  10. lemma OAI.SLEExactGauge.stoppedMarkedScale_pos line 54
  11. lemma OAI.SLEExactGauge.stoppedMarkedCenter_eq line 59
  12. lemma OAI.SLEExactGauge.source_stoppedDriver_measurable line 76
  13. lemma OAI.SLEExactGauge.source_stoppedMarkedCenter_measurable line 83
  14. lemma OAI.SLEExactGauge.source_stoppedMarkedScale_measurable line 89
  15. lemma OAI.SLEExactGauge.source_stoppedMarkedUnit_measurable line 95
  16. lemma OAI.SLEExactGauge.source_stopped_live_iff_killedChart_im_pos line 102
  17. lemma OAI.SLEExactGauge.source_stopped_live_measurable line 112
  18. lemma OAI.SLEExactGauge.source_stoppedMarkedGood_measurable line 123
  19. lemma OAI.SLEExactGauge.stoppedMarkedScale_eq_on_live line 131
  20. lemma OAI.SLEExactGauge.stoppedMarkedUnit_im_on_live line 140
  21. theorem OAI.SLEExactGauge.source_stoppedMarkedState_geometry line 150

    Source documentation

    Exact geometric data required by the conformal dense estimate.

    theorem source_stoppedMarkedState_geometry (z : ℂ) (ω : Ω)
    (hz : z ∈ survivingDomain (γ ω) (τ ω)) :
    let w := stoppedMarkedUnit κ B γ G τ z ω
…

    Mentions: OAI.SLEExactGauge.survivingDomain, OAI.SLEExactGauge.stoppedMarkedUnit