DenseCoverAdaptedTests.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Adapted dense-visit tests at the manuscript's actual logarithmic multiplicity and linear index window. This proves the failure calculation without independence between the tests.

theorem OAI.SLEExactGauge.complement_inter_bound_of_success_lower line 15

theorem OAI.SLEExactGauge.adapted_failures_Icc_bound line 31

Source documentation

The exact finite window can start at any filtration index.

theorem adapted_failures_Icc_bound
    {Ω : Type*} [mΩ : MeasurableSpace Ω] (μ : Measure Ω)
    (F : Filtration ℕ mΩ) (failure : ℕ → Set Ω)
    (hmeas : ∀ j, MeasurableSet[F (j + 1)] (failure j))
    (q : ℝ≥0∞)
    (hstep : ∀ j (B : Set Ω), MeasurableSet[F j] B →
      μ (B ∩ failure j) ≤ q * μ B)
    (a b : ℕ) (hab : a ≤ b) :
    μ (⋂ j ∈ Finset.Icc a b, failure j) ≤ q ^ (b + 1 - a) * μ univ := by
…

theorem OAI.SLEExactGauge.cover_window_failure_bound line 60

Source documentation

Conditional success bounds at the actual scale yield the stretched exponential bound for failure of every test in the cover window.

theorem cover_window_failure_bound
    {Ω : Type*} [mΩ : MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
    (F : Filtration ℕ mΩ) (success : ℕ → Set Ω)
    (hmeas : ∀ j, MeasurableSet[F (j + 1)] (success j))
    (n : ℕ) (hn : 1 ≤ n)
    (hstep : ∀ j (B : Set Ω), MeasurableSet[F j] B →
      ENNReal.ofReal (1 / Real.sqrt (n : ℝ)) * μ B ≤ μ (B ∩ success j)) :
    μ (⋂ j ∈ coverTestWindow n, (success j)ᶜ) ≤
      ENNReal.ofReal (Real.exp (-Real.sqrt (n : ℝ) / 4)) := by
…

Mentions: OAI.SLEExactGauge.coverTestWindow

theorem OAI.SLEExactGauge.denseVisit_cover_window_failure line 90