OAI/Probability/SLE/Gauge/ActualRibbonIteration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SLEExactGauge.ribbonIntegerFront line 20
2. lemma OAI.SLEExactGauge.ribbonIntegerFront_monotone line 23
3. def OAI.SLEExactGauge.actualRibbonSuccess line 30
4. theorem OAI.SLEExactGauge.actual_ribbon_successes_lower_bound line 37

   Source documentation

   Actual fronts turn the quantitative step estimate into a product lower bound for the exact physical passage-and-mass events.

   theorem actual_ribbon_successes_lower_bound
       {Ω : Type*} [mΩ : MeasurableSpace Ω] (μ : Measure Ω) (ℱ : Filtration ℝ≥0 mΩ)
       (γ : Ω → ℝ≥0 → ℂ) (ha : Adapted ℱ (fun t ω => γ ω t))
       (hc : ∀ ω, Continuous (γ ω)) (g : C(ℂ, ℝ)) (hg0 : ∀ ω, g (γ ω 0) = 0)
       (P : ℂ → ℂ) (hemb : Topology.IsClosedEmbedding (fun z : closedRibbon => P z))
       (ε κ v c : ℝ) (q : ℝ≥0∞)
       (hstep : ∀ (n : ℕ) (A : Set Ω),
         MeasurableSet[(ribbonFrontStop_stopping ℱ g γ ha hc ((n : ℝ) + 1)).measurableSpace] A →
         A ⊆ GoodRibbonPrefix γ (ribbonIntegerFront g γ n) P ε →
           q * μ A ≤ μ (A ∩ actualRibbonSuccess γ g P ε κ v c n)) :
       ∀ N : ℕ, q ^ N * μ (GoodRibbonPrefix γ (ribbonIntegerFront g γ 0) P ε) ≤
         μ (GoodRibbonPrefix γ (ribbonIntegerFront g γ 0) P ε ∩
   …

   Mentions: OAI.SLEExactGauge.ribbonFrontStop_stopping, OAI.SLEExactGauge.GoodRibbonPrefix, OAI.SLEExactGauge.ribbonIntegerFront, OAI.SLEExactGauge.actualRibbonSuccess