SmallScale

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

Rate constants and the small-scale mass bound

This file fixes the dimension-dependent constants of the percolation estimate, records the arithmetic of the admissibility gate, and bounds the expected small-scale weighted cube mass along one deterministic path.

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

The dimension-dependent normalization used in the fixed-path Gaussian tail.

Equations

• Algsuperdiff.Section5.Percolation.fixedPathTailScaleConst d = 8 * (↑d + 1) * (1 + HCPolySupport.IndependentSums.gammaTriangleConst 2 * Algsuperdiff.Section5.Percolation.fixedPathLayerConst d)

theorem Algsuperdiff.Section5.Percolation.fixedPathTailScaleConst_pos (d : ℕ) : 0 < fixedPathTailScaleConst d

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

The dimension-dependent prefactor in the large-scale union bound.

Equations

• Algsuperdiff.Section5.Percolation.pathBoundPrefactorConst d = 3 ^ d * Algsuperdiff.Probability.geomTailConst 1

theorem Algsuperdiff.Section5.Percolation.pathBoundPrefactorConst_pos (d : ℕ) : 0 < pathBoundPrefactorConst d

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

A dimension-dependent threshold that absorbs the fixed-path, large-scale, mean, path-counting, and geometric-series constants.

Equations

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

theorem Algsuperdiff.Section5.Percolation.pathBoundGateConst_pos (d : ℕ) : 0 < pathBoundGateConst d

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

The fixed-path quadratic rate after the two-event union bound.

Equations

• Algsuperdiff.Section5.Percolation.fixedPathRateConst d = (2 * Algsuperdiff.Section5.Percolation.fixedPathTailScaleConst d ^ 2)⁻¹

theorem Algsuperdiff.Section5.Percolation.fixedPathRateConst_pos (d : ℕ) : 0 < fixedPathRateConst d

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

The rate retained after absorbing the finite path count.

Equations

• Algsuperdiff.Section5.Percolation.pathLengthRateConst d = Algsuperdiff.Section5.Percolation.fixedPathRateConst d / 2

theorem Algsuperdiff.Section5.Percolation.pathLengthRateConst_pos (d : ℕ) : 0 < pathLengthRateConst d

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

The rate retained after summing over all possible excess path lengths.

Equations

• Algsuperdiff.Section5.Percolation.pathBoundRateConst d = Algsuperdiff.Section5.Percolation.pathLengthRateConst d / 2

theorem Algsuperdiff.Section5.Percolation.pathBoundRateConst_pos (d : ℕ) : 0 < pathBoundRateConst d

theorem Algsuperdiff.Section5.Percolation.gateConst_le_product {d : ℕ} {a T lam : ℝ} (ha : 1 < a) (hlam : 0 < lam) (hgate : pathBoundGateConst d * lam⁻¹ * (a - 1)⁻¹ ≤ T) : pathBoundGateConst d ≤ (a - 1) * T * lam

theorem Algsuperdiff.Section5.Percolation.fixedPathTailScale_core_le (d : ℕ) : 8 * (↑d + 1) * (HCPolySupport.IndependentSums.gammaTriangleConst 2 * fixedPathLayerConst d) ≤ fixedPathTailScaleConst d

theorem Algsuperdiff.Section5.Percolation.fixedPathTailScale_dimension_le (d : ℕ) : 8 * (↑d + 1) ≤ fixedPathTailScaleConst d

theorem Algsuperdiff.Section5.Percolation.gateConst_scale_le (d : ℕ) : 64 * (↑d + 1) * fixedPathTailScaleConst d ≤ pathBoundGateConst d

theorem Algsuperdiff.Section5.Percolation.gateConst_prefactor_le (d : ℕ) : 64 * (↑d + 1) * pathBoundPrefactorConst d ≤ pathBoundGateConst d

theorem Algsuperdiff.Section5.Percolation.gateConst_one_le (d : ℕ) : 64 * (↑d + 1) ≤ pathBoundGateConst d

theorem Algsuperdiff.Section5.Percolation.entropy_le_fixedPathRate_of_gate {d : ℕ} {a T lam : ℝ} (ha : 1 < a) (hlam : 0 < lam) (hgate : pathBoundGateConst d * lam⁻¹ * (a - 1)⁻¹ ≤ T) : 8 * (↑d + 1) ≤ fixedPathRateConst d * ((a - 1) * T * lam) ^ 2

theorem Algsuperdiff.Section5.Percolation.exp_neg_sq_div_four_le_inv {T : ℝ} (hT : 8 ≤ T) : Real.exp (-(T ^ 2 / 4)) ≤ T⁻¹

theorem Algsuperdiff.Section5.Percolation.geomTailConst_half_sub_one_le {d : ℕ} {a : ℝ} (ha : 1 < a) (had : a ≤ ↑d) : Probability.geomTailConst ((a - 1) / 2) ≤ 2 * (↑d + 1) * (a - 1)⁻¹

theorem Algsuperdiff.Section5.Percolation.two_mul_le_three_pow (L : ℕ) : 2 * L ≤ 3 ^ L

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

The deterministic mean of the weighted inflated-cube count over a finite set of scales.

Equations

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

theorem Algsuperdiff.Section5.Percolation.weightedCubeMassOn_eq_centered_add_expected {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (P : MeasureTheory.Measure Ω) (B : ℕ → Site d → Set Ω) (Γ : List (Site d)) (scales : Finset ℕ) (ω : Ω) : weightedCubeMassOn B Γ scales ω = centeredWeightedCubeMassOn P B Γ scales ω + expectedWeightedCubeMassOn P B Γ scales

Weighted mass is its centered part plus its deterministic mean.

theorem Algsuperdiff.Section5.Percolation.expectedWeightedCubeMassOn_small_le {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (P : MeasureTheory.Measure Ω) (B : ℕ → Site d → Set Ω) (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 Γ) : expectedWeightedCubeMassOn P B Γ (smallScales Γ) ≤ 2 * 3 ^ d * ↑Γ.length * Real.exp (-(T ^ 2 / 4)) * Probability.geomTailConst 1

The deterministic mean over all small scales is bounded by a geometric multiple of the path length.