FiniteCoverAssembly.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite selected/missed covers and measurable envelopes for their costs.

def OAI.SLEExactGauge.wholeSausageMeasure line 15
Source documentation
The one-mesh charge is a measure, so disjoint candidates can be summed.
```
def wholeSausageMeasure (κ : ℝ) (γ : ℝ≥0 → ℂ) (v : ℝ) : Measure ℂ :=
…
```
lemma OAI.SLEExactGauge.wholeSausageMeasure_apply line 18

theorem OAI.SLEExactGauge.hausdorff_le_liminf_finite_cover_envelope line 25

Source documentation

Pointwise existence of finite covers suffices. Their selection need not be measurable when a measurable envelope controls their costs.

theorem hausdorff_le_liminf_finite_cover_envelope
    (h : ℝ → ℝ) (E : Set ℂ) (δ : ℕ → ℝ≥0∞)
    (hδ : Tendsto δ atTop (𝓝 0)) (Z : ℕ → ℝ≥0∞)
    (hcovers : ∀ n, ∃ (N : ℕ) (U : Fin N → Set ℂ),
      E ⊆ ⋃ j, U j ∧ (∀ j, ediam (U j) ≤ δ n) ∧
        ∑ j, extendedGauge h (ediam (U j)) ≤ Z n) :
    hausdorffGauge h E ≤ liminf Z atTop := by
…

Mentions: OAI.SLEExactGauge.extendedGauge, OAI.SLEExactGauge.hausdorffGauge

theorem OAI.SLEExactGauge.expected_hausdorff_le_of_finite_cover_envelopes line 38

Source documentation

Fatou applied to the cost envelope, rather than to a chosen random cover.

theorem expected_hausdorff_le_of_finite_cover_envelopes
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (h : ℝ → ℝ) (E : Ω → Set ℂ) (δ : ℕ → ℝ≥0∞)
    (hδ : Tendsto δ atTop (𝓝 0)) (Z : ℕ → Ω → ℝ≥0∞)
    (hZ : ∀ n, AEMeasurable (Z n) P)
    (hcovers : ∀ᵐ ω ∂P, ∀ n, ∃ (N : ℕ) (U : Fin N → Set ℂ),
      E ω ⊆ ⋃ j, U j ∧ (∀ j, ediam (U j) ≤ δ n) ∧
        ∑ j, extendedGauge h (ediam (U j)) ≤ Z n ω)
    (C : ℝ≥0∞) (hcost : liminf (fun n => ∫⁻ ω, Z n ω ∂P) atTop ≤ C) :
    (∫⁻ ω, hausdorffGauge h (E ω) ∂P) ≤ C := by
…

Mentions: OAI.SLEExactGauge.extendedGauge, OAI.SLEExactGauge.hausdorffGauge

theorem OAI.SLEExactGauge.exists_finite_selected_missed_cover line 59

Source documentation

Disjoint candidate disks and all missed cells give a genuine finite cover with cost paid by one spatial measure and the missed-cell sum.

theorem exists_finite_selected_missed_cover
    {ι η : Type*} (I : Finset ι) (M : Finset η)
    (x : ι → ℂ) (r : ι → ℝ) (Q : η → Set ℂ)
    (E A : Set ℂ) (ν : Measure ℂ) (h : ℝ → ℝ)
    (R : ℝ) (hr : ∀ i ∈ I, r i ≤ R) (δ C : ℝ≥0∞)
    (hA : ∀ i ∈ I, closedBall (x i) (r i) ⊆ A)
    (hcost : ∀ i ∈ I,
      extendedGauge h (ediam (closedBall (x i) (4 * r i))) ≤
        C * ν (closedBall (x i) (r i)))
    (hdisk : ∀ i ∈ I, ediam (closedBall (x i) (4 * r i)) ≤ δ)
    (hmiss : ∀ k ∈ M, ediam (Q k) ≤ δ)
    (hcell : ∀ z ∈ E, (∃ i ∈ I, z ∈ closedBall (x i) (r i)) ∨
…

Mentions: OAI.SLEExactGauge.extendedGauge

theorem OAI.SLEExactGauge.expected_hausdorff_le_of_finite_sausage_covers line 111

Source documentation

The finite cover can be chosen independently at every sample and scale. Only its common sausage charge and missed-cell envelope need measurability.

theorem expected_hausdorff_le_of_finite_sausage_covers
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (h : ℝ → ℝ) (E : Ω → Set ℂ) (δ : ℕ → ℝ≥0∞)
    (hδ : Tendsto δ atTop (𝓝 0))
    (v : ℕ → ℝ) (hv : ∀ n, 0 < v n) (R : ℝ) (C : ℝ≥0)
    (error : ℕ → Ω → ℝ≥0∞) (herr : ∀ n, AEMeasurable (error n) P)
    (herrlim : Tendsto (fun n => ∫⁻ ω, error n ω ∂P) atTop (𝓝 0))
    (hcovers : ∀ᵐ ω ∂P, ∀ n, ∃ (N : ℕ) (U : Fin N → Set ℂ),
      E ω ⊆ ⋃ j, U j ∧ (∀ j, ediam (U j) ≤ δ n) ∧
        ∑ j, extendedGauge h (ediam (U j)) ≤
…

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