DenseCoverUpperReduction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Candidate and missed-cell tests imply the dense-cover upper bound.

theorem OAI.SLEExactGauge.expected_hausdorff_le_of_candidate_disks line 16

Source documentation

Spatial selection, missed-cell probability bounds, and one-mesh charging produce the upper Hausdorff expectation. No measurable choice of disks is needed.

theorem expected_hausdorff_le_of_candidate_disks
    {Ω ι η : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (h : ℝ → ℝ) (E : Ω → Set ℂ)
    (I : ℕ → Ω → Finset ι) (M : ℕ → Finset η)
    (x : ℕ → ι → ℂ) (r : ℕ → ι → ℝ) (Q : ℕ → η → Set ℂ)
    (missed : ℕ → η → Set Ω)
    (hmissmeas : ∀ n k, k ∈ M n → MeasurableSet (missed n k))
    (v : ℕ → ℝ) (hv : ∀ n, 0 < v n) (R : ℝ) (C : ℝ≥0)
    (δ : ℕ → ℝ≥0∞) (hδ : Tendsto δ atTop (𝓝 0))
…

Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE