SmallWavesArith

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

Arithmetic and combinatorics for the small-waves lane

1. Its cardinality and the resulting (1 + log N)^{1/σ} penalty are produced exactly as LatticeCount does for the annulus.
2. The interchange Σ_{n ≤ m} Σ_{k=n-1}^{m} = Σ_{k ≤ m} Σ_{n ≤ (k+1) ∧ m}, an identity in ℝ≥0∞ (Tonelli, no side condition).
3. The geometric partial weight, the manuscript's 4 s^{-1}.
4. That absorption is proved here, explicitly.

References

• ABK26, l.ratio.of.good.scales.for.k, Step 2.
• ABK26, e.maxy.bound and e.powerofGammasigma.

1. The lattice cube as a Finset, and its penalty

noncomputable def Algsuperdiff.Section4.Provider.Proportion.latticeCubeFinset (d : ℕ) (j outer : ℤ) : Finset (Fin d → ℤ)

The lattice cube as a Finset: the proved set Support.latticeCubeSet cut out of the enclosing index box. This is the 𝒢₁b maximum's index set.

Equations

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

theorem Algsuperdiff.Section4.Provider.Proportion.mem_latticeCubeFinset_iff {d : ℕ} {j outer : ℤ} (hj : j ≤ outer) {v : Fin d → ℤ} : v ∈ latticeCubeFinset d j outer ↔ v ∈ Support.latticeCubeSet d j outer

theorem Algsuperdiff.Section4.Provider.Proportion.card_latticeCubeFinset_le (d : ℕ) {j outer : ℤ} : (latticeCubeFinset d j outer).card ≤ 3 ^ (d * ((outer - j).toNat + 1))

The count. #(3^j ℤ^d ∩ □_outer) ≤ 3^{d(outer−j+1)}.

theorem Algsuperdiff.Section4.Provider.Proportion.log_card_latticeCubeFinset_le (d : ℕ) {j outer : ℤ} : Real.log ↑(latticeCubeFinset d j outer).card ≤ ↑d * (↑(outer - j).toNat + 1) * Real.log 3

theorem Algsuperdiff.Section4.Provider.Proportion.log_card_cube_le_annulusPenalty_rpow_sub_one (d : ℕ) {sigma : ℝ} (hsigma : 0 < sigma) (j outer : ℤ) : Real.log ↑(latticeCubeFinset d j outer).card ≤ annulusPenalty d sigma (outer - j).toNat ^ sigma - 1

The isBigOWith_fmax interface log(#S) ≤ c^σ − 1, discharged at the lattice cube by the same penalty LatticeCount uses for the annulus.

2. The ℝ≥0∞ interchange

theorem Algsuperdiff.Section4.Provider.Proportion.finsetIcc_sum_eq_tsum (g : ℤ → ENNReal) (a b : ℤ) : ∑ k ∈ Finset.Icc a b, g k = ∑' (k : ℤ), if a ≤ k ∧ k ≤ b then g k else 0

A finite Finset.Icc block written as a guarded tsum.

theorem Algsuperdiff.Section4.Provider.Proportion.tsum_block_comm (w g : ℤ → ENNReal) (m : ℤ) : (∑' (n : ℤ), if n ≤ m then w n * ∑ k ∈ Finset.Icc (n - 1) m, g k else 0) = ∑' (k : ℤ), if k ≤ m then (∑' (n : ℤ), if n ≤ min (k + 1) m then w n else 0) * g k else 0

The 𝒢₁b interchange, as an identity. Tonelli in ℝ≥0∞ does the swap unconditionally: everything is nonnegative, so there is no summability side condition.

3. The geometric partial weight

noncomputable def Algsuperdiff.Section4.Provider.Proportion.gwG1b (s : ℝ) (t : ℤ) : ENNReal

The event's own geometric weight 3^{-s(m-n)/4}, in ℝ≥0∞ and in the exact spelling of the frozen 𝒢₁ definition.

Equations

• Algsuperdiff.Section4.Provider.Proportion.gwG1b s t = ENNReal.ofReal (Real.rpow 3 (-(1 / 4) * s * ↑t))

noncomputable def Algsuperdiff.Section4.Provider.Proportion.g1bConst (s : ℝ) : ℝ

The manuscript's interchange constant 4 s^{-1}, in the explicit form the ℝ≥0∞ proof produces.

Equations

• Algsuperdiff.Section4.Provider.Proportion.g1bConst s = Real.rpow 3 (s / 2) * (12 / s)

theorem Algsuperdiff.Section4.Provider.Proportion.g1bConst_pos {s : ℝ} (hs : 0 < s) : 0 < g1bConst s

theorem Algsuperdiff.Section4.Provider.Proportion.tsum_partialWeight_le {s : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (m k : ℤ) : (∑' (n : ℤ), if n ≤ min (k + 1) m then gwG1b s (m - n) else 0) ≤ ENNReal.ofReal (g1bConst s) * gwG1b s (m - k)

The partial weight bound, proved. For n ≤ k + 1 the weight 3^{-s(m-n)/4} is at most 3^{s/2} times the two-sided Appendix-D weight at rate s/4, so the guarded n-sum is O(s^{-1}) times 3^{-s(m-k)/4}.

4. Absorbing the lattice-max penalty into the discount

theorem Algsuperdiff.Section4.Provider.Proportion.rpow_mul_penalty_sq_le (d : ℕ) {s : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (p : ℕ) : Real.rpow 3 (-(s / 8 * ↑p)) * (1 + ↑d * (↑p + 1) * Real.log 3) ≤ 8 / s * (1 + 2 * ↑d * Real.log 3)

The uniform tail scale of the 𝒢₁b array. The lattice-max penalty at σ = 2, squared, is 1 + d(p+1)log 3, which grows linearly in the scale gap `p = m

• k; the array's built-in discount 3^{-s p/8}absorbs it at the cost of one power ofs^{-1}`.