Weights

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

Concentration for scale arrays — geometric weight sums (Step 1 input)

The row weights wt t k j = 3^{-t |k-j|} are summable over j ∈ ℤ with ∑_j wt t k j = (1 + 3^{-t}) / (1 - 3^{-t}) ≤ 3 / t for t ∈ (0, 1].

Deviation from the paper's constant

The paper (e.YktoZk.twosided, Step 1) uses the sharp bound ∑_{ℓ∈ℤ} 3^{-(s/2)|ℓ|} ≤ 4 s⁻¹, which forces the threshold prefactor 6 in e.no.bad.scales.twosided. The sharp bound requires log 3 > 1.055, a delicate numeric estimate. We instead prove the clean bound ∑_{ℓ∈ℤ} 3^{-t|ℓ|} ≤ 3/t (i.e. ≤ 6 s⁻¹ with t = s/2), which needs only log 3 > 1. This inflates the final threshold prefactor from 6 to 9 (6 = 2·3 becomes 9 = 3·3), a documented and harmless change of universal constant; the exponential rate is unaffected.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.log_three_gt_one : 1 < Real.log 3

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.log_three_lt_two : Real.log 3 < 2

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.three_rpow_neg_le {t : ℝ} (ht : 0 < t) (ht1 : t ≤ 1) : 3 ^ (-t) ≤ (3 - t) / (3 + t)

The transcendental core of the geometric bound: 3^{-t} ≤ (3-t)/(3+t) for t ∈ (0,1], proved via the quadratic lower bound exp x ≥ 1 + x + x²/2.

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.summable_pow_natAbs {q : ℝ} (hq0 : 0 ≤ q) (hq1 : q < 1) : Summable fun (ℓ : ℤ) => q ^ ℓ.natAbs

The ℤ-summability of ℓ ↦ q^{|ℓ|} for q ∈ [0,1).

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.tsum_pnat_geometric {q : ℝ} (hq0 : 0 ≤ q) (hq1 : q < 1) : ∑' (n : ℕ+), q ^ ↑n = q / (1 - q)

The ℕ⁺-sum of a geometric series equals q/(1-q).

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.tsum_int_pow_natAbs {q : ℝ} (hq0 : 0 ≤ q) (hq1 : q < 1) : ∑' (ℓ : ℤ), q ^ ℓ.natAbs = (1 + q) / (1 - q)

The ℤ-sum of q^{|ℓ|} equals (1+q)/(1-q).

theorem Algsuperdiff.Section4.Probability.ScalesConcentration.tsum_three_rpow_neg_abs_le {t : ℝ} (ht : 0 < t) (ht1 : t ≤ 1) : ∑' (ℓ : ℤ), 3 ^ (-(t * ↑ℓ.natAbs)) ≤ 3 / t

Geometric weight bound (Step 1 input): for t ∈ (0,1], ∑_{ℓ∈ℤ} 3^{-t|ℓ|} ≤ 3/t.