ShrinkingCoverAtoms.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The nonatomicity step of mass:construction: a squared atom is bounded by every squared covering mass sum. Fatou therefore rules out all atoms at once, without a countable union over points.

lemma OAI.SLEExactGauge.singleton_sq_le_cover_sum line 21

Source documentation

One atom is charged to one cell in any finite cover.

lemma singleton_sq_le_cover_sum (μ : Measure X) (I : Finset ℕ) (C : ℕ → Set X)
    {x : X} (hcover : ∃ i ∈ I, x ∈ C i) :
    (μ {x})^2 ≤ ∑ i ∈ I, (μ (C i))^2 := by
…

theorem OAI.SLEExactGauge.ae_null_singletons_on_of_square_bounds line 31

Source documentation

Vanishing expected upper bounds for squared atoms exclude every atom on a set simultaneously almost surely.

theorem ae_null_singletons_on_of_square_bounds (P : Measure Ω) (μ : Ω → Measure X)
    (K : Set X) (A : ℕ → Ω → ℝ≥0∞) (hA : ∀ n, Measurable (A n))
    (hbound : ∀ ω x, x ∈ K → ∀ n, (μ ω {x})^2 ≤ A n ω)
    (hlim : Tendsto (fun n => ∫⁻ ω, A n ω ∂P) atTop (𝓝 0)) :
    ∀ᵐ ω ∂P, ∀ x ∈ K, μ ω {x}=0 := by
…

theorem OAI.SLEExactGauge.ae_null_singletons_on_of_cover_sums line 50

Source documentation

The finite-cover form used for compact exhaustion. Cover diameters need not be named here: all geometric decay is captured in the expected squared mass sum.

theorem ae_null_singletons_on_of_cover_sums (P : Measure Ω) (μ : Ω → Measure X)
    (hμ : Measurable μ) (K : Set X) (I : ℕ → Finset ℕ) (C : ℕ → ℕ → Set X)
    (hC : ∀ n i, MeasurableSet (C n i))
    (hcover : ∀ n x, x ∈ K → ∃ i ∈ I n, x ∈ C n i)
    (hlim : Tendsto (fun n => ∫⁻ ω, ∑ i ∈ I n, (μ ω (C n i))^2 ∂P) atTop (𝓝 0)) :
    ∀ᵐ ω ∂P, ∀ x ∈ K, μ ω {x}=0 := by
…

theorem OAI.SLEExactGauge.ae_nullSingletonClass_of_exhaustion line 65

Source documentation

A countable covering of the whole space upgrades the compact-by-compact criterion to a nonatomic random measure.

theorem ae_nullSingletonClass_of_exhaustion (P : Measure Ω) (μ : Ω → Measure X)
    (K : ℕ → Set X) (hcover : ∀ x, ∃ j, x ∈ K j)
    (hK : ∀ j, ∀ᵐ ω ∂P, ∀ x ∈ K j, μ ω {x}=0) :
    ∀ᵐ ω ∂P, NullSingletonClass (μ ω) := by
…