CubeMass

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Weighted inflated-cube masses

This file records the bad-vertex count along one deterministic path, the centered indicator of an inflated cube event, and the coloured average bound for the scale-L weighted mass of the cubes that a path touches.

noncomputable def Algsuperdiff.Section5.Percolation.inflatedVertexCount {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (Γ : List (Site d)) (ω : Ω) : ℝ

The number of distinct vertices of Γ at which the all-scale inflated bad event occurs, represented as a real random variable.

Equations

• Algsuperdiff.Section5.Percolation.inflatedVertexCount B Γ ω = ∑ z ∈ Γ.toFinset, (Algsuperdiff.Section5.Percolation.inflatedBadSet B z).indicator (fun (x : Ω) => 1) ω

theorem Algsuperdiff.Section5.Percolation.coe_inflatedCubeCount_eq {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (L : ℕ) (Γ : List (Site d)) (ω : Ω) : ↑(inflatedCubeCount B L Γ ω) = ∑ v ∈ touchingCenters L Γ, (inflatedBadEvent B L v).indicator (fun (x : Ω) => 1) ω

The scale-L inflated-cube count is the sum of the corresponding event indicators over the touched cubes.

noncomputable def Algsuperdiff.Section5.Percolation.centeredInflatedCubeIndicator {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (P : MeasureTheory.Measure Ω) (B : ℕ → Site d → Set Ω) (L : ℕ) (v : Site d) (ω : Ω) : ℝ

The centered indicator of one inflated cube event.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section5.Percolation.isBigO_gammaTwo_average_centeredInflatedCubeIndicator {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (B : ℕ → Site d → Set Ω) (hB : ∀ (L : ℕ) (z : Site d), MeasurableSet (B L z)) (hsep : SepIndep P B) (L : ℕ) (Γ : List (Site d)) (R : ℝ) (hR : 1 ≤ R) (htail : ∀ v ∈ touchingCenters L Γ, P.real (inflatedBadEvent B L v) ≤ Real.exp (-R ^ 2)) : HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma 2) (fun (ω : Ω) => (↑(touchingCenters L Γ).card)⁻¹ * ∑ v ∈ touchingCenters L Γ, centeredInflatedCubeIndicator P B L v ω) (HCPolySupport.IndependentSums.gammaTriangleConst 2 * HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst 2 * (√(3 ^ d) * (√↑(touchingCenters L Γ).card / ↑(touchingCenters L Γ).card)) * (2 * R⁻¹))

The centered inflated-cube indicators along one path satisfy the coloured finite-range concentration estimate.

noncomputable def Algsuperdiff.Section5.Percolation.centeredWeightedCubeMassAt {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (P : MeasureTheory.Measure Ω) (B : ℕ → Site d → Set Ω) (Γ : List (Site d)) (L : ℕ) (ω : Ω) : ℝ

The centered scale-L contribution to the weighted cube mass.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section5.Percolation.isBigO_gammaTwo_centeredWeightedCubeMassAt {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (B : ℕ → Site d → Set Ω) (hB : ∀ (L : ℕ) (z : Site d), MeasurableSet (B L z)) (hsep : SepIndep P B) (L : ℕ) (Γ : List (Site d)) (R : ℝ) (hR : 1 ≤ R) (htail : ∀ v ∈ touchingCenters L Γ, P.real (inflatedBadEvent B L v) ≤ Real.exp (-R ^ 2)) : HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma 2) (centeredWeightedCubeMassAt P B Γ L) (3 ^ L * ↑(touchingCenters L Γ).card * (HCPolySupport.IndependentSums.gammaTriangleConst 2 * HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst 2 * (√(3 ^ d) * (√↑(touchingCenters L Γ).card / ↑(touchingCenters L Γ).card)) * (2 * R⁻¹)))

The colored estimate for one centered, scale-weighted cube count.