DenseCoverExpectation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The expected explicit-gauge cost of the actual finite candidate cover. The leading constant is chosen before the compact interior cutoff; only the vanishing missed-cell prefactor is allowed to depend on that cutoff.

def OAI.SLEExactGauge.denseMissedProbabilityBound line 19
theorem OAI.SLEExactGauge.dense_missed_cost_tendsto_zero line 22

theorem OAI.SLEExactGauge.expected_hausdorff_of_dense_candidates line 63

Source documentation

A uniform candidate charge and the actual stretched-exponential missed bound give the upper expectation. C is fixed before R, K, and D.

theorem expected_hausdorff_of_dense_candidates
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (hγ : ∀ ω, Continuous (γ ω))
    {T b c : ℝ} (hT : 0 < T) (hb : 0 < b) (hc : 0 < c)
    (h : ℝ → ℝ) (hh : IsGauge h) (hf : HasSmallRadiusFormula h (hFormula κ)) :
    ∃ C : ℝ≥0, 0 < C ∧ ∀ (R : ℝ), 0 ≤ R → ∀ K : Set ℂ,
      K ⊆ closedBall 0 R → ∀ (v : ℕ → ℝ), (∀ n, 0 < v n) →
      ∀ (D : ℝ), 0 ≤ D →
      (∀ᶠ n : ℕ in atTop, ∀ ij ∈ retainedCoverGridIndex R (coverRadius T n) K,
        P {ω | denseMissedCell κ T b c (v n) n ij (γ ω)} ≤ denseMissedProbabilityBound κ T D n) →
…

Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.IsGauge, OAI.SLEExactGauge.HasSmallRadiusFormula, OAI.SLEExactGauge.hFormula, OAI.SLEExactGauge.retainedCoverGridIndex, OAI.SLEExactGauge.coverRadius, OAI.SLEExactGauge.denseMissedCell, OAI.SLEExactGauge.denseMissedProbabilityBound