OAI/Probability/SLE/Gauge/ExpectedCoverCharge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SLEExactGauge.expected_hausdorff_le_of_sausage_charged_covers line 17

   Source documentation

   A shrinking cover whose selected part is charged to a single sausage mesh and whose expected residual cost vanishes has the desired uniform Hausdorff expectation bound. The hypothesis describes actual covers.

   theorem expected_hausdorff_le_of_sausage_charged_covers
       {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
       (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
       (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
       (h : ℝ → ℝ) (hh : IsGauge h) (E : Ω → Set ℂ)
       (U : ℕ → Ω → ℕ → Set ℂ) (δ : ℕ → ℝ≥0∞)
       (hδ : Tendsto δ atTop (𝓝 0))
       (hcover : ∀ᵐ ω ∂P, ∀ n, E ω ⊆ ⋃ j, U n ω j)
       (hdiam : ∀ᵐ ω ∂P, ∀ n j, ediam (U n ω j) ≤ δ n)
       (hmeas : ∀ n, AEMeasurable
         (fun ω => ∑' j, extendedGauge h (ediam (U n ω j))) P)
       (v : ℕ → ℝ) (hv : ∀ n, 0 < v n) (R : ℝ) (C : ℝ≥0)
   …

   Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.IsGauge, OAI.SLEExactGauge.extendedGauge