DenseCoverMassTests.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Actual sausage tests at successive stopping times. Their terminal candidate implication is deterministic, whereas their failure calculation uses only information observable at each test endpoint.

def OAI.SLEExactGauge.stoppedWholeSausageCharge line 21
theorem OAI.SLEExactGauge.stoppedWholeSausageCharge_le_whole line 25
theorem OAI.SLEExactGauge.stoppedWholeSausageCharge_finite line 34
theorem OAI.SLEExactGauge.stoppedWholeSausageCharge_measurable_at_stop line 42
def OAI.SLEExactGauge.clockStopFiltration line 52
def OAI.SLEExactGauge.stoppedMassTest line 60
theorem OAI.SLEExactGauge.stoppedMassTest_measurable_at_stop line 65

theorem OAI.SLEExactGauge.no_terminal_candidate_subset_stopped_failures line 77

Source documentation

No terminal candidate forces failure of every earlier adapted test. The terminal candidate is never put inside a finite change of measure.

theorem no_terminal_candidate_subset_stopped_failures
    {Ω : Type*} (κ v : ℝ) (f : Ω → C(ℝ≥0, ℂ))
    (τ : ℕ → Ω → WithTop ℝ≥0) (D : ℕ → Set ℂ) (b : ℕ → ℝ) (I : Finset ℕ) :
    {ω | ∀ j ∈ I, wholeSausageCharge κ (f ω) v (D j) < ENNReal.ofReal (b j)} ⊆
      ⋂ j ∈ I, (stoppedMassTest κ v f (τ (j + 1)) (D j) (b j))ᶜ := by
…

Mentions: OAI.SLEExactGauge.wholeSausageCharge, OAI.SLEExactGauge.stoppedMassTest

theorem OAI.SLEExactGauge.stoppedMassTests_cover_failure line 90

Source documentation

The actual successive stopped-sausage tests give the stretched exponential missed-candidate bound under their finite stopped law.

theorem stoppedMassTests_cover_failure
    {Ω : Type*} [mΩ : MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
    (ℱ : Filtration ℝ≥0 mΩ)
    (γ : Ω → ℝ≥0 → ℂ) (ha : Adapted ℱ (fun t ω => γ ω t))
    (hc : ∀ ω, Continuous (γ ω))
    (τ : ℕ → Ω → WithTop ℝ≥0) (hτ : ∀ j, IsStoppingTime ℱ (τ j))
    (hmono : ∀ ω, Monotone (fun j => τ j ω))
    (κ v : ℝ) (D : ℕ → Set ℂ) (b : ℕ → ℝ) (n : ℕ) (hn : 1 ≤ n)
    (hstep : ∀ j (B : Set Ω), MeasurableSet[(hτ j).measurableSpace] B →
      ENNReal.ofReal (1 / Real.sqrt (n : ℝ)) * μ B ≤
        μ (B ∩ stoppedMassTest κ v (sourceTracePath γ hc) (τ (j + 1)) (D j) (b j))) :
    μ {ω | ∀ j ∈ coverTestWindow n,
…

Mentions: OAI.SLEExactGauge.stoppedMassTest, OAI.SLEExactGauge.sourceTracePath, OAI.SLEExactGauge.coverTestWindow