OAI/Probability/SLE/Gauge/RetainedPassageExtraction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Countable-to-finite retention in the ribbon passage argument. The loss is bounded for every varying early-containment event by the same discarded set. Sausage exceptions are subtracted unconditionally.

  1. theorem OAI.SLEExactGauge.finite_retention_of_countable_cover line 16
  2. theorem OAI.SLEExactGauge.varying_events_after_finite_retention line 56

    Source documentation

    Discarding one small set preserves a fixed fraction of every member of a varying family; no independence is involved.

    theorem varying_events_after_finite_retention
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsFiniteMeasure P]
    (E : Set Ω) (D : ℕ → Set Ω) (G : ℕ → Set Ω)
    (hE : MeasurableSet E) (hD : ∀ i, MeasurableSet (D i))
    (hcover : P (E \ ⋃ i, D i) = 0)
    (q : ℝ) (hq : 0 < q)
    (hG : ∀ n, ENNReal.ofReal q ≤ P (G n ∩ E)) :
    ∃ N : ℕ, ∀ n, ENNReal.ofReal (q / 2) ≤
      P (G n ∩ E ∩ ⋃ i ∈ Finset.range N, D i) := by
…