RibbonPassageMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The last probabilistic transfer in the ribbon step: a finite deterministic list of retained time intervals permits subtracting one unconditional small-sausage exception from the varying passage events. The sausage estimate is never conditioned on passage.

theorem OAI.SLEExactGauge.ribbon_passage_mass_of_eventually_finite_intervals line 20

Source documentation

The finite-list subtraction step of rc:step. Passage may select a different deterministic interval on each sample and at each mesh.

theorem ribbon_passage_mass_of_eventually_finite_intervals
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (I : Finset (ℝ≥0 × ℝ≥0)) (hI : ∀ J ∈ I, J.1 < J.2)
    (v : ℕ → ℝ) (hv : ∀ n, 0 < v n) (hlim : Tendsto v atTop (𝓝 0))
    (G : ℕ → Set Ω) (q : ℝ) (hq : 0 < q)
    (hG : ∀ᶠ n in atTop, ENNReal.ofReal q ≤ P (G n))
    (physicalMass : ℕ → Ω → ℝ≥0∞) (passage : ℕ → Ω → Prop)
    (c : ℝ) (hc : 0 < c)
    (htransfer : ∀ᶠ n in atTop, ∀ ω, ω ∈ G n → passage n ω ∧
      ∃ J ∈ I, ENNReal.ofReal c *
…

Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE

theorem OAI.SLEExactGauge.ribbon_passage_mass_of_finite_intervals line 73

Source documentation

A version with transfer and probability bounds at every index.

theorem ribbon_passage_mass_of_finite_intervals
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (I : Finset (ℝ≥0 × ℝ≥0)) (hI : ∀ J ∈ I, J.1 < J.2)
    (v : ℕ → ℝ) (hv : ∀ n, 0 < v n) (hlim : Tendsto v atTop (𝓝 0))
    (G : ℕ → Set Ω) (q : ℝ) (hq : 0 < q)
    (hG : ∀ n, ENNReal.ofReal q ≤ P (G n))
    (physicalMass : ℕ → Ω → ℝ≥0∞) (passage : ℕ → Ω → Prop)
    (c : ℝ) (hc : 0 < c)
    (htransfer : ∀ n ω, ω ∈ G n → passage n ω ∧
      ∃ J ∈ I, ENNReal.ofReal c *
…

Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE

theorem OAI.SLEExactGauge.ribbon_mass_of_finite_intervals line 94

Source documentation

The same finite-list transfer with passage already included in G n.

theorem ribbon_mass_of_finite_intervals
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (I : Finset (ℝ≥0 × ℝ≥0)) (hI : ∀ J ∈ I, J.1 < J.2)
    (v : ℕ → ℝ) (hv : ∀ n, 0 < v n) (hlim : Tendsto v atTop (𝓝 0))
    (G : ℕ → Set Ω) (q : ℝ) (hq : 0 < q)
    (hG : ∀ n, ENNReal.ofReal q ≤ P (G n))
    (physicalMass : ℕ → Ω → ℝ≥0∞) (c : ℝ) (hc : 0 < c)
    (htransfer : ∀ n ω, ω ∈ G n →
      ∃ J ∈ I, ENNReal.ofReal c *
        sourceSausageMass κ (γ ω) J.1 J.2 (v n) ≤ physicalMass n ω) :
…

Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.sourceSausageMass