The step-sum slot count and the rung-weight product

This file provides two elementary estimates used by the summed truncation bound apd:eq:total_high_weight_norm in the proof of apd:thm:one_step_truncation_error: the sum over Trotter steps of the layer-slot binomials, and the closed form of the rung-weight product ∏ w_j.

Main results

• sum_pow_le: Σ_{d=1}^{r} d^m ≤ (r+1)^{m+1}/(m+1).
• sum_choose_mul_le: the slot count Σ_{d=1}^{r} C(dΓ, K) ≤ ((r+1)Γ)^{K+1} / (Γ · (K+1)!).
• prod_rungW_eq: ∏_{j=2}^{n+1} w_j = (k_h−1)^n ∏_{i=1}^{n} (i+c).
• prod_shift_le, prod_shift_ratio: comparison of ∏_{i=1}^{n}(i+c) with the shifted product ∏_{i=2}^{n+1}(i+c).

The slot count

Summing the per-step bound over the r Trotter steps uses

Σ_{d=1}^{r} C(dΓ, K) ≤ ((r+1)Γ)^{K+1} / (Γ · (K+1)!),

which is sum_choose_mul_le below. The paper uses it with K = m* for the leading sector; the ladder assembly (Lean4LPD.Ladder.ChainBound) applies it once per sector K = k. Two remarks.

The right-hand side is reproduced exactly. The proof has two steps, C(n,k) ≤ n^k/k! and Σ_{d=1}^{r} d^K ≤ (r+1)^{K+1}/(K+1), and their composition is identically the right-hand side above; nothing further is discarded.

Γ is a positive layer count. It is a natural number because it counts the layers of the decomposition H = ∑_{γ=1}^{Γ} H_γ in apd:thm:one_step_truncation_error, and C(dΓ, K) counts layer slots, so the natural-number type is not an extra restriction relative to the paper's theorem.

The rung-weight product

With w_j = (k_h−1)(j−1+c) the rung product has the closed form

∏_{j=2}^{m*+2} w_j = (k_h−1)^{m*+1} ∏_{i=1}^{m*+1} (i+c),

which is prod_rungW_eq. The estimate displayed with apd:eq:total_high_weight_norm is written in terms of the shifted product ∏_{j=2}^{m*+2} (j+c). prod_shift_le shows that the shifted product is the larger of the two, and prod_shift_ratio that their ratio is exactly (m*+2+c)/(1+c). Bounds built on the exact product are therefore stronger than the paper's statement and imply it.

The companion estimate ∏_{i=1}^{n}(i+c) ≤ n!·(e·n)^c is not in this file: it needs real powers and a harmonic-sum bound, and is proved in Lean4LPD.Constants.AssemblyBound as prod_add_one_le_factorial_exp_rpow (with prod_shifted_le_factorial_exp_rpow for the shifted product).

theorem Lean4LPD.pow_le_sub_pow {d : ℝ} (hd : 1 ≤ d) (m : ℕ) : (↑m + 1) * d ^ m ≤ (d + 1) ^ (m + 1) - d ^ (m + 1)

d^m ≤ ((d+1)^{m+1} − d^{m+1})/(m+1) for d ≥ 1, the integral comparison behind the slot count, in the form Bernoulli's inequality supplies it.

theorem Lean4LPD.sum_pow_le (m r : ℕ) : ∑ i ∈ Finset.range r, (↑i + 1) ^ m ≤ (↑r + 1) ^ (m + 1) / (↑m + 1)

Σ_{d=1}^{r} d^m ≤ (r+1)^{m+1}/(m+1), the integral comparison, by telescoping pow_le_sub_pow. Written over range r with body (i+1)^m so that no ℕ subtraction appears.

theorem Lean4LPD.sum_choose_mul_le (K r G : ℕ) (hG : 1 ≤ G) : ∑ i ∈ Finset.range r, ↑(((i + 1) * G).choose K) ≤ ((↑r + 1) * ↑G) ^ (K + 1) / (↑G * ↑(K + 1).factorial)

The slot count. The sum over Trotter steps of the layer-slot binomials, the step that leads to apd:eq:total_high_weight_norm in the proof of apd:thm:one_step_truncation_error:

Σ_{d=1}^{r} C(dΓ, K) ≤ ((r+1)Γ)^{K+1} / (Γ · (K+1)!).

Γ is a positive natural number, because it is a layer count and C(dΓ, K) counts layer slots (see the module docstring). The two steps — C(n,k) ≤ n^k/k! and sum_pow_le — reproduce the right-hand side exactly, so nothing is thrown away.

theorem Lean4LPD.prod_rungW_eq (kh1 c : ℝ) (n : ℕ) : ∏ i ∈ Finset.range n, rungW kh1 c (i + 2) = kh1 ^ n * ∏ i ∈ Finset.range n, (↑i + 1 + c)

The rung product in closed form. ∏_{j=2}^{n+1} w_j = (k_h−1)^n ∏_{i=1}^{n} (i+c), written over range n. The second factor is smaller than the shifted product ∏_{j=2}^{n+1}(j+c) in which the estimate of apd:eq:total_high_weight_norm is displayed — see prod_shift_le and prod_shift_ratio.

theorem Lean4LPD.prod_shift_le {c : ℝ} (hc : 0 ≤ c) (n : ℕ) : ∏ i ∈ Finset.range n, (↑i + 1 + c) ≤ ∏ i ∈ Finset.range n, (↑i + 2 + c)

The exact product is dominated by the shifted one: ∏_{i=1}^{n}(i+c) ≤ ∏_{i=2}^{n+1}(i+c) for c ≥ 0, termwise. Hence a bound proved with the exact product of prod_rungW_eq implies the same bound with the shifted product, the form displayed in the paper.

theorem Lean4LPD.prod_shift_ratio (c : ℝ) (n : ℕ) : (∏ i ∈ Finset.range n, (↑i + 2 + c)) * (1 + c) = (∏ i ∈ Finset.range n, (↑i + 1 + c)) * (↑n + 1 + c)

The shifted product exceeds the exact one by exactly the factor (n+1+c)/(1+c): (∏_{i<n}(i+2+c)) · (1+c) = (∏_{i<n}(i+1+c)) · (n+1+c). Both products telescope against each other, so the gap between them is a single ratio rather than a factor accumulating with n.