FixedPath

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

Fixed-path multiscale concentration

This file assembles, for one deterministic path, the Gaussian tail parameter of an inflated cube event, the finite partial sums of the scale-weighted inflated-cube counts, and the small-scale Orlicz bound for those sums.

noncomputable def Algsuperdiff.Section5.Percolation.inflatedTailRate (a T : ℝ) (L : ℕ) : ℝ

The natural Gaussian tail parameter at scale L after absorbing the volume of an inflated cube.

Equations

• Algsuperdiff.Section5.Percolation.inflatedTailRate a T L = T / 2 * 3 ^ (a * ↑L / 2)

theorem Algsuperdiff.Section5.Percolation.one_le_inflatedTailRate {a T : ℝ} (ha : 0 ≤ a) (hT : 2 ≤ T) (L : ℕ) : 1 ≤ inflatedTailRate a T L

The inflated tail parameter is at least one in the admissible range.

theorem Algsuperdiff.Section5.Percolation.measureReal_inflatedBadEvent_le_tailRate {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (P : MeasureTheory.Measure Ω) (B : ℕ → Site d → Set Ω) (a T : ℝ) (hB : ∀ (L : ℕ) (z : Site d), P.real (B L z) ≤ Real.exp (-(T ^ 2 * 3 ^ (a * ↑L)))) (ha : 1 ≤ a) (hT : 2 * (↑d + 1) ≤ T) (L : ℕ) (v : Site d) : P.real (inflatedBadEvent B L v) ≤ Real.exp (-inflatedTailRate a T L ^ 2)

The absorbed inflated-event tail is bounded by the square of its natural scale parameter.

noncomputable def Algsuperdiff.Section5.Percolation.fixedPathLayerConst (d : ℕ) : ℝ

A dimension-dependent constant for the centered contribution of one scale along a fixed path.

Equations

• Algsuperdiff.Section5.Percolation.fixedPathLayerConst d = 8 * HCPolySupport.IndependentSums.gammaTriangleConst 2 * HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst 2 * 3 ^ (2 * d)

theorem Algsuperdiff.Section5.Percolation.fixedPathLayerConst_pos (d : ℕ) : 0 < fixedPathLayerConst d

theorem Algsuperdiff.Section5.Percolation.measurable_coe_inflatedCubeCount {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} {B : ℕ → Site d → Set Ω} (hB : ∀ (L : ℕ) (z : Site d), MeasurableSet (B L z)) (L : ℕ) (Γ : List (Site d)) : Measurable fun (ω : Ω) => ↑(inflatedCubeCount B L Γ ω)

The real-valued scale-L inflated-cube count is measurable.

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

A finite partial sum of the scale-weighted inflated-cube counts.

Equations

• Algsuperdiff.Section5.Percolation.weightedCubeMassOn B Γ scales ω = ∑ L ∈ scales, 3 ^ L * ↑(Algsuperdiff.Section5.Percolation.inflatedCubeCount B L Γ ω)

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

The event that some finite partial scale sum exceeds r. This avoids any convention for a divergent real series while expressing the nonnegative infinite sum used in the percolation argument.

Equations

• Algsuperdiff.Section5.Percolation.weightedCubeEvent B Γ r = {ω : Ω | ∃ (scales : Finset ℕ), r < Algsuperdiff.Section5.Percolation.weightedCubeMassOn B Γ scales ω}

def Algsuperdiff.Section5.Percolation.pathBlock {d : ℕ} (L : ℕ) (Γ : List (Site d)) (b : ℕ) : List (Site d)

The b-th consecutive block of at most 3^L path vertices.

Equations

• Algsuperdiff.Section5.Percolation.pathBlock L Γ b = List.take (3 ^ L) (List.drop (b * 3 ^ L) Γ)

theorem Algsuperdiff.Section5.Percolation.card_touchingCenters_le_three_pow_mul_blocks {d L : ℕ} {Γ : List (Site d)} (hΓ : IsPath Γ) : (touchingCenters L Γ).card ≤ 3 ^ d * (Γ.length / 3 ^ L + 1)

A lattice path of vertex length n touches at most 3^d (⌊n / 3^L⌋ + 1) canonical scale-L cubes.

theorem Algsuperdiff.Section5.Percolation.three_pow_mul_card_touchingCenters_le {d L : ℕ} {Γ : List (Site d)} (hΓ : IsPath Γ) (hsmall : 3 ^ L ≤ Γ.length) : 3 ^ L * (touchingCenters L Γ).card ≤ 2 * 3 ^ d * Γ.length

At scales no larger than a path, side length times the number of touched cubes is at most twice the dimension factor times the vertex length.

theorem Algsuperdiff.Section5.Percolation.isBigO_gammaTwo_centeredWeightedCubeMassAt_le {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (B : ℕ → Site d → Set Ω) (hBmeas : ∀ (L : ℕ) (z : Site d), MeasurableSet (B L z)) (hsep : SepIndep P B) (a T : ℝ) (hBtail : ∀ (L : ℕ) (z : Site d), P.real (B L z) ≤ Real.exp (-(T ^ 2 * 3 ^ (a * ↑L)))) (ha : 1 ≤ a) (hT : 2 * (↑d + 1) ≤ T) (L : ℕ) (Γ : List (Site d)) (hΓ : IsPath Γ) (hsmall : 3 ^ L ≤ Γ.length) : HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma 2) (centeredWeightedCubeMassAt P B Γ L) (fixedPathLayerConst d * √↑Γ.length * T⁻¹ * 3 ^ (-((a - 1) / 2 * ↑L)))

At a scale no larger than the path length, the centered weighted cube count has the square-root path-size concentration scale and the geometric decay 3^{-(a-1)L/2}.

def Algsuperdiff.Section5.Percolation.smallScales {d : ℕ} (Γ : List (Site d)) : Finset ℕ

The finite set of scales whose triadic side length does not exceed the vertex length of Γ.

Equations

• Algsuperdiff.Section5.Percolation.smallScales Γ = {L ∈ Finset.range (Γ.length + 1) | 3 ^ L ≤ Γ.length}

@[simp]

theorem Algsuperdiff.Section5.Percolation.mem_smallScales_iff {d L : ℕ} {Γ : List (Site d)} : L ∈ smallScales Γ ↔ 3 ^ L ≤ Γ.length

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

The centered weighted mass over a finite set of scales.

Equations

• Algsuperdiff.Section5.Percolation.centeredWeightedCubeMassOn P B Γ scales ω = ∑ L ∈ scales, Algsuperdiff.Section5.Percolation.centeredWeightedCubeMassAt P B Γ L ω

theorem Algsuperdiff.Section5.Percolation.isBigO_gammaTwo_centeredWeightedCubeMassOn_small {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (B : ℕ → Site d → Set Ω) (hBmeas : ∀ (L : ℕ) (z : Site d), MeasurableSet (B L z)) (hsep : SepIndep P B) (a T : ℝ) (hBtail : ∀ (L : ℕ) (z : Site d), P.real (B L z) ≤ Real.exp (-(T ^ 2 * 3 ^ (a * ↑L)))) (ha : 1 < a) (hT : 2 * (↑d + 1) ≤ T) (Γ : List (Site d)) (hΓ : IsPath Γ) (hΓpos : 0 < Γ.length) : HCPolySupport.IndependentSums.IsBigO P (HCPolySupport.IndependentSums.gammaSigma 2) (centeredWeightedCubeMassOn P B Γ (smallScales Γ)) (HCPolySupport.IndependentSums.gammaTriangleConst 2 * fixedPathLayerConst d * √↑Γ.length * T⁻¹ * Probability.geomTailConst ((a - 1) / 2))

The centered mass over all small scales has a uniform Gaussian scale controlled by the geometric closure at exponent (a-1)/2.