The entry factor E_ν ≤ ε_ν^{(ν)}(1 + 2β)

This file defines the scalar quantities of the multi-jump analysis (apd:rmk:multijump) — the rung weights w_m, the j-jump block norms ε_j^{(ν)}, the expansion parameter β and the entry factor E_ν of apd:eq:composition_majorant — and proves the entry-factor bound apd:eq:entry_bound with the constant 2 where the paper has 4e.

A single layer may act on one Pauli with j anti-commuting rotations, raising it by j rungs in one step. Such a jump may overshoot the ladder: a Pauli below rung 1 — weight ≤ w₁, its norm controlled by the reservoir bound ‖O‖ — may end above rung ν after one layer; this needs j > ν and is therefore not a composition of ν. All of these contributions are collected in the entry factor

E_ν := ∑_{j≥ν} ε_j^{(ν)}, ε_j^{(ν)} := (w_{ν+j} · sin dt)^j / j!,

which the paper bounds by E_ν ≤ ε_ν^{(ν)}(1 + 4eβ) for β := 2e w₂ sin(dt) ≤ 1/2.

Main definitions

• rungW: the rung weight w_m = (k_h − 1)(m − 1 + c), c = k_o/(k_h − 1).
• epsJump: the j-jump block norm ε_j^{(ν)}.
• betaOf: the expansion parameter β = 2e·w₂·a.
• entryFactor: the entry factor E_ν, an infinite sum.

Main results

• epsJump_ratio: ε_{j+1}^{(ν)} ≤ β · ε_j^{(ν)} for j ≥ ν ≥ 1.
• entryFactor_le_geom: E_ν ≤ ε_ν^{(ν)}/(1 − β) for every β < 1.
• entryFactor_le: E_ν ≤ ε_ν^{(ν)}(1 + 2β) for β ≤ 1/2 (apd:eq:entry_bound).
• one_add_two_mul_le_source: 1 + 2β ≤ 1 + 4eβ, the comparison with the paper's constant.

The proof: geometric decay of the terms

The terms of E_ν decay geometrically with ratio β,

ε_{j+1}^{(ν)} ≤ β · ε_j^{(ν)} for every j ≥ ν ≥ 1,

because (w_{ν+j+1}/w_{ν+j})^j ≤ (1 + 1/j)^j ≤ e and w_{ν+j+1}·a/(j+1) ≤ 2w₂a = β/e. Summing the geometric series gives E_ν ≤ ε_ν^{(ν)}/(1 − β), hence ≤ ε_ν^{(ν)}(1 + 2β) for β ≤ 1/2. This is stronger than the paper's statement (1 + 4eβ), since 4e ≈ 10.87, and implies it. The hypothesis β ≤ 1/2 is not needed for the geometric form: E_ν ≤ ε_ν^{(ν)}/(1−β) holds for every β < 1, a larger range than the paper's parameter regime. In that regime the step-count condition r ≥ 8e²·w₂·αt of apd:eq:multijump_factor, together with sin(dt) ≤ αt/r, gives 4eβ ≤ 1, i.e. β ≤ 1/(4e) < 1/2, so the hypothesis of entryFactor_le is always available there.

The constant 1 + 2β is smaller than the paper's 1 + 4eβ; the bound c₀ ≤ 2 of Lean4LPD.cZero_le_two is proved with the paper's constant. See Lean4LPD.Constants.C0.

k_o = 0 (hence c = 0, hence w₁ = 0) is the extremal case of the estimates below, not an exception to them; only k_h ≥ 2, i.e. k_h − 1 > 0, is required.

def Lean4LPD.rungW (kh1 c : ℝ) (m : ℕ) : ℝ

The rung weight w_m = (k_h − 1)(m − 1 + c) with c = k_o/(k_h − 1), that is w_m = k_o + (m − 1)(k_h − 1): the largest weight reachable from weight k_o with m − 1 anti-commuting k_h-local rotations, and the threshold of rung m in apd:eq:def_high_weight_norm. It is real-valued so that no ℕ subtraction occurs. kh1 is k_h − 1. Note w₂ = (k_h−1)(1+c) = k_o+k_h−1.

Equations

• Lean4LPD.rungW kh1 c m = kh1 * (↑m - 1 + c)

noncomputable def Lean4LPD.epsJump (kh1 c a : ℝ) (j nu : ℕ) : ℝ

The j-jump block norm into rung ν, ε_j^{(ν)} = (w_{ν+j}·a)^j / j! (apd:rmk:multijump), with a = sin(dt).

Equations

• Lean4LPD.epsJump kh1 c a j nu = (Lean4LPD.rungW kh1 c (nu + j) * a) ^ j / ↑j.factorial

noncomputable def Lean4LPD.betaOf (kh1 c a : ℝ) : ℝ

The expansion parameter β = 2e·w₂·a of the multi-jump analysis (apd:rmk:multijump), with a = sin(dt).

Equations

• Lean4LPD.betaOf kh1 c a = 2 * Real.exp 1 * Lean4LPD.rungW kh1 c 2 * a

theorem Lean4LPD.rungW_nonneg {kh1 c : ℝ} (hkh : 0 < kh1) (hc : 0 ≤ c) {m : ℕ} (hm : 1 ≤ m) : 0 ≤ rungW kh1 c m

theorem Lean4LPD.epsJump_nonneg {kh1 c a : ℝ} (hkh : 0 < kh1) (hc : 0 ≤ c) (ha : 0 ≤ a) (j nu : ℕ) (h : 1 ≤ nu + j) : 0 ≤ epsJump kh1 c a j nu

theorem Lean4LPD.one_add_inv_pow_le_exp_one {j : ℕ} (hj : 1 ≤ j) : (1 + 1 / ↑j) ^ j ≤ Real.exp 1

(1 + 1/j)^j ≤ e for j ≥ 1.

theorem Lean4LPD.epsJump_ratio {kh1 c a : ℝ} (hkh : 0 < kh1) (hc : 0 ≤ c) (ha : 0 ≤ a) {j nu : ℕ} (hnu : 1 ≤ nu) (hj : nu ≤ j) : epsJump kh1 c a (j + 1) nu ≤ betaOf kh1 c a * epsJump kh1 c a j nu

The term-ratio bound: for j ≥ ν ≥ 1,

ε_{j+1}^{(ν)} ≤ β · ε_j^{(ν)}.

This geometric decay of the terms is what drives entryFactor_le_geom. Two estimates, both termwise: w_{ν+j+1} ≤ w_{ν+j}·(1 + 1/j) because ν+j−1+c ≥ j, and w_{ν+j+1} ≤ w₂·(ν+j) ≤ 2w₂·j because ν ≤ j.

noncomputable def Lean4LPD.entryFactor (kh1 c a : ℝ) (nu : ℕ) : ℝ

The entry factor E_ν = ∑_{j≥ν} ε_j^{(ν)} of apd:eq:composition_majorant, written as a tsum over the shift j = ν + i. This is the only infinite sum in the multi-jump development; the ladder itself takes E abstractly (see Lean4LPD.MultiLadder).

Equations

• Lean4LPD.entryFactor kh1 c a nu = ∑' (i : ℕ), Lean4LPD.epsJump kh1 c a (nu + i) nu

theorem Lean4LPD.entryFactor_le_geom {kh1 c a : ℝ} (hkh : 0 < kh1) (hc : 0 ≤ c) (ha : 0 ≤ a) {nu : ℕ} (hnu : 1 ≤ nu) (hb1 : betaOf kh1 c a < 1) : entryFactor kh1 c a nu ≤ epsJump kh1 c a nu nu / (1 - betaOf kh1 c a)

The entry-factor bound, geometric form. For every β < 1,

E_ν ≤ ε_ν^{(ν)} / (1 − β).

No β ≤ 1/2 is needed; that hypothesis enters only in converting to the affine form entryFactor_le. The proof sums the geometric majorant supplied by epsJump_ratio.

theorem Lean4LPD.entryFactor_le {kh1 c a : ℝ} (hkh : 0 < kh1) (hc : 0 ≤ c) (ha : 0 ≤ a) {nu : ℕ} (hnu : 1 ≤ nu) (hb : betaOf kh1 c a ≤ 1 / 2) : entryFactor kh1 c a nu ≤ epsJump kh1 c a nu nu * (1 + 2 * betaOf kh1 c a)

The entry-factor bound, affine form (apd:eq:entry_bound):

E_ν ≤ ε_ν^{(ν)} · (1 + 2β) for β ≤ 1/2.

The constant 2 is stronger than the paper's statement, which has 4e ≈ 10.87 in its place. Since 1 + 2β ≤ 1 + 4eβ for β ≥ 0 (one_add_two_mul_le_source), the bound with (1 + 4eβ) follows, so every downstream use of that factor remains valid.

theorem Lean4LPD.one_add_two_mul_le_source {b : ℝ} (hb : 0 ≤ b) : 1 + 2 * b ≤ 1 + 4 * Real.exp 1 * b

Comparison with the paper's constant: 1 + 2β ≤ 1 + 4eβ, since 2 ≤ 4e. Stated as a lemma so that the sharpening in entryFactor_le is a checked comparison rather than prose only.