OAI/Probability/SLE/Gauge/RibbonGoodPrefix.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Narrow actual prefixes are measurable in the possibly infinite front past. They are exactly the physical information used to reconstruct the history at the next integer front.

  1. def OAI.SLEExactGauge.ribbonCore line 19
  2. lemma OAI.SLEExactGauge.ribbonCore_isClosed line 22
  3. def OAI.SLEExactGauge.GoodRibbonPrefix line 38
  4. lemma OAI.SLEExactGauge.stoppedAtPath_eval_time line 43
  5. lemma OAI.SLEExactGauge.stoppedAtPath_range_iff line 51
  6. lemma OAI.SLEExactGauge.measurableSet_path_range_closed line 62
  7. theorem OAI.SLEExactGauge.goodRibbonPrefix_measurable line 77

    Source documentation

    The successful physical prefix belongs to the actual front past; failed samples need not have a finite front time.

    theorem goodRibbonPrefix_measurable
    {Ω : Type*} [mΩ : MeasurableSpace Ω] (ℱ : Filtration ℝ≥0 mΩ)
    (γ : Ω → ℝ≥0 → ℂ) (ha : Adapted ℱ (fun t ω => γ ω t))
    (hc : ∀ ω, Continuous (γ ω))
    (τ : Ω → WithTop ℝ≥0) (hτ : IsStoppingTime ℱ τ)
    (P : ℂ → ℂ) (he : Topology.IsClosedEmbedding (fun z : closedRibbon => P z)) (ε : ℝ) :
    MeasurableSet[hτ.measurableSpace] (GoodRibbonPrefix γ τ P ε) := by
…

    Mentions: OAI.SLEExactGauge.GoodRibbonPrefix

  8. lemma OAI.SLEExactGauge.RibbonHistory.goodRibbonPrefix line 111