OAI/Probability/SLE/Gauge/CoverLimits.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SLEExactGauge.hausdorff_le_liminf_cover_cost line 18

   Source documentation

   Cover costs control the Hausdorff limit even when they do not converge.

   theorem hausdorff_le_liminf_cover_cost
       (h : ℝ → ℝ) (hh : IsGauge h) (E : Set ℂ)
       (U : ℕ → ℕ → Set ℂ) (δ : ℕ → ℝ≥0∞)
       (hδ : Tendsto δ atTop (𝓝 0))
       (hcover : ∀ n, E ⊆ ⋃ j, U n j)
       (hdiam : ∀ n j, ediam (U n j) ≤ δ n) :
       hausdorffGauge h E ≤
         liminf (fun n => ∑' j, extendedGauge h (ediam (U n j))) atTop := by
   …

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

2. theorem OAI.SLEExactGauge.expected_hausdorff_le_of_shrinking_covers line 35

   Source documentation

   Fatou's lemma for measurable costs of actual covers, with a limiting expectation bound rather than an assumption about the target measure.

   theorem expected_hausdorff_le_of_shrinking_covers
       {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
       (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)
       (C : ℝ≥0∞)
       (hcost : liminf (fun n => ∫⁻ ω,
         ∑' j, extendedGauge h (ediam (U n ω j)) ∂P) atTop ≤ C) :
   …

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

3. theorem OAI.SLEExactGauge.disjoint_cover_charge line 61

   Source documentation

   Disjoint candidate sets are all paid for by the same spatial measure.

   theorem disjoint_cover_charge {ι : Type*} (I : Finset ι)
       (ν : Measure ℂ) (D : ι → Set ℂ) (A : Set ℂ)
       (hdisj : (I : Set ι).PairwiseDisjoint D)
       (hmeas : ∀ i ∈ I, MeasurableSet (D i))
       (hsub : ∀ i ∈ I, D i ⊆ A)
       (cost : ι → ℝ≥0∞) (C : ℝ≥0∞)
       (hcost : ∀ i ∈ I, cost i ≤ C * ν (D i)) :
       ∑ i ∈ I, cost i ≤ C * ν A := by
   …

4. theorem OAI.SLEExactGauge.expected_measure_iUnion_le line 78

   Source documentation

   Continuity from below retains a uniform expectation bound as both the time cutoff and the distance from the real boundary are removed.

   theorem expected_measure_iUnion_le
       {Ω X : Type*} [MeasurableSpace Ω] [MeasurableSpace X]
       (P : Measure Ω) (ν : Measure X) (E : ℕ → Ω → Set X)
       (hmono : ∀ ω, Monotone (fun n => E n ω))
       (hmeas : ∀ n, AEMeasurable (fun ω => ν (E n ω)) P)
       (C : ℝ≥0∞) (hbound : ∀ n, (∫⁻ ω, ν (E n ω) ∂P) ≤ C) :
       (∫⁻ ω, ν (⋃ n, E n ω) ∂P) ≤ C := by
   …

5. theorem OAI.SLEExactGauge.measure_inter_eq_interior_of_null_boundary line 91

   Source documentation

   Adding a set contained in a fixed null boundary costs no measure.

   theorem measure_inter_eq_interior_of_null_boundary
       {X : Type*} [MeasurableSpace X] (ν : Measure X)
       (E A H : Set X)
       (hboundary : ν (E ∩ A ∩ Hᶜ) = 0) :
       ν (E ∩ A) = ν (E ∩ A ∩ H) := by
   …