The multi-jump ladder and its first-passage majorant

This file defines the abstract multi-jump ladder MultiLadder, in which one layer may raise the mass by several rungs at once, and proves for it the first-passage majorant apd:eq:composition_majorant of apd:rmk:multijump (MultiLadder.le_majorant), together with the monotonicity of the majorant in the number of layers.

The rotations of one layer have pairwise disjoint supports, so several of them can anticommute with the same Pauli string. When j ≥ 2 of them do, the string moves up j rungs within that single layer. By apd:thm:layer_inflow the corresponding block of the layer's action is bounded in norm by ε_j^{(m)} := (w_{m+j} sin dt)^j / j!. The power of sin(dt) is j, as for j successive one-rung moves. The difference lies in the number of layers consumed, one instead of j, and in the rung the jump starts from, which is m - j instead of m - 1.

The contribution of multi-jumps therefore has to enter the recursion as additional inflow terms. It cannot be expressed as a constant factor in front of apd:eq:layer_cumulation, because that bound is proportional to C(T,m) and hence zero whenever T < m, while mass can cross the truncation threshold after a single layer. apd:rmk:multijump illustrates this with O = Z₁Z₂Z₃, the layer {X₁X₄, X₂X₅, X₃X₆} and w* = 5: after one layer the evolved observable contains a Pauli string of weight 6, reached by three simultaneous jumps, with coefficient sin³(dt). The bound that accounts for these inflows is the first-passage majorant apd:eq:composition_majorant, formalized here.

What the hypothesis says, and what it already assumes

In apd:rmk:multijump the recursion reads

N_m^{(T)} ≤ N_m^{(T-1)} + ∑_{j≥1} ε_j^{(m)} N_{m-j}^{(T-1)}, with N_ν := ‖O‖ for ν ≤ 0.

Substituting the convention N_ν := ‖O‖ splits the sum at j = m:

∑_{j≥1} ε_j^{(m)} N_{m-j} = ∑_{j=1}^{m-1} ε_j^{(m)} N_{m-j} + (∑_{j≥m} ε_j^{(m)}) · M,

and the second bracket is the entry factor E_m := ∑_{j≥m} ε_j^{(m)}. It collects every way of leaving the reservoir in one jump and landing above rung m, including the overshoot jumps j > m, which start below rung 1 and which a plain sum over compositions of m would omit. MultiLadder.step is that already-substituted form. Two consequences:

• the infinite sum does not appear here. E is an abstract field, related to ε by nothing at all, so the theorem below reads "if the recursion holds with some E, the majorant holds with that same E" — more general than the paper's statement. The series ∑_{j≥m} appears exactly once in this development, as Lean4LPD.entryFactor in Lean4LPD/Constants/Entry.lean, where it is bounded (apd:eq:entry_bound);
• N_ν = M for ν ≤ 0 is the reservoir bound, justified by unitary invariance of the 2-norm together with truncation only decreasing every N. Here it is part of the hypothesis step (the term E m * M), and it is discharged by the Pauli model in Lean4LPD/Pauli/LayerLadder.lean (PauliString.pauliMultiLadder), just as Ladder.reservoir is for the single-jump ladder.

The recursive form of the chain sum

The majorant sums over strictly increasing rung sequences 0 < ν₁ < ⋯ < ν_k = m. Peeling the last jump gives the recursion that chain is defined by. chain_diag below then proves the statement of apd:rmk:multijump that the all-ones term reproduces the layer-cumulation bound, which is the check that the definition is the intended object rather than merely a plausible one.

Main definitions

• chain ε E k m: the total weight of the first-passage paths to rung m with exactly k jumps.
• MultiLadder ε E M: the damped ladder with every jump length retained.
• MultiLadder.majorant: the bound of apd:eq:composition_majorant, as a function of m, T.
• MultiLadder.trivialMultiLadder: the zero family, showing that the structure is inhabited.

Main results

• chain_eq_zero_of_lt: a path to rung m uses at most m jumps.
• chain_diag: the all-ones term is E 1 · ∏_{i=2}^{m} ε_1^{(i)}.
• MultiLadder.le_majorant: the first-passage majorant, N m T ≤ majorant ε E M m T.
• MultiLadder.majorant_mono: the majorant is monotone in the number of layers.

def Lean4LPD.chain (eps : ℕ → ℕ → ℝ) (E : ℕ → ℝ) : ℕ → ℕ → ℝ

The inner chain sum of apd:eq:composition_majorant, defined by peeling the last jump: chain ε E k m is the total weight of all first-passage paths that leave the reservoir once and climb to rung m through exactly k jumps at strictly increasing rungs.

chain ε E 0 m = 0, chain ε E 1 m = E m, chain ε E (k+2) m = ∑_{j=1}^{m-1} ε_j^{(m)} · chain ε E (k+1) (m-j).

The recursion is on the number of jumps k, not on the rung m, so it is structural. The sum over Finset.Ico 1 m keeps 1 ≤ j < m, hence 1 ≤ m - j: no ℕ truncated subtraction is ever evaluated outside its intended range.

Equations

• Lean4LPD.chain eps E 0 x✝ = 0
• Lean4LPD.chain eps E 1 x✝ = E x✝
• Lean4LPD.chain eps E k.succ.succ x✝ = ∑ j ∈ Finset.Ico 1 x✝, eps j x✝ * Lean4LPD.chain eps E (k + 1) (x✝ - j)

@[simp]

theorem Lean4LPD.chain_zero (eps : ℕ → ℕ → ℝ) (E : ℕ → ℝ) (m : ℕ) : chain eps E 0 m = 0

@[simp]

theorem Lean4LPD.chain_one (eps : ℕ → ℕ → ℝ) (E : ℕ → ℝ) (m : ℕ) : chain eps E 1 m = E m

theorem Lean4LPD.chain_succ_succ (eps : ℕ → ℕ → ℝ) (E : ℕ → ℝ) (k m : ℕ) : chain eps E (k + 2) m = ∑ j ∈ Finset.Ico 1 m, eps j m * chain eps E (k + 1) (m - j)

theorem Lean4LPD.chain_nonneg {eps : ℕ → ℕ → ℝ} {E : ℕ → ℝ} (heps : ∀ (j m : ℕ), 0 ≤ eps j m) (hE : ∀ (m : ℕ), 0 ≤ E m) (k m : ℕ) : 0 ≤ chain eps E k m

theorem Lean4LPD.chain_eq_zero_of_lt {eps : ℕ → ℕ → ℝ} {E : ℕ → ℝ} (k m : ℕ) : 1 ≤ m → m < k → chain eps E k m = 0

A path to rung m ≥ 1 cannot use more than m jumps, each jump climbing at least one rung. This is what makes the outer sum of apd:eq:composition_majorant run to min(m, T) even though majorant below sums to T.

theorem Lean4LPD.chain_diag {eps : ℕ → ℕ → ℝ} {E : ℕ → ℝ} (m : ℕ) : 1 ≤ m → chain eps E m m = E 1 * ∏ i ∈ Finset.Ico 2 (m + 1), eps 1 i

The all-ones term is the single-jump layer-cumulation bound. Formalizes the statement of apd:rmk:multijump that the term of the majorant with k = m jumps, all of length one (so ν_i = i), coincides with the bound apd:eq:layer_cumulation:

chain ε E m m = E 1 · ∏_{i=2}^{m} ε_1^{(i)}.

A composition of m into m parts has every part equal to one: in the defining recursion a last jump of length j ≥ 2 would leave m - 1 jumps to reach rung m - j < m - 1, and that term vanishes by chain_eq_zero_of_lt. With ε_1^{(i)} = w_{i+1} sin(dt) this product is sin^{m-1}(dt) ∏_{j=3}^{m+1} w_j, which is Lean4LPD.layer_cumulation's product with the entry rung's factor replaced by E 1 — the one place the two bounds differ, and the reason the entry factor is kept separate.

structure Lean4LPD.MultiLadder (eps : ℕ → ℕ → ℝ) (E : ℕ → ℝ) (M : ℝ) : Type

A multi-jump ladder: the damped ladder with every jump length retained.

N m T is the mass strictly above rung m after T disjoint-support layers, eps j m is the j-jump block norm into rung m, E m the entry factor out of the reservoir into rung m, and M the total mass. See the module docstring for why step is already in substituted form and for what that does and does not assume.

• N : ℕ → ℕ → ℝ

  Mass strictly above rung m after T layers.

• nonneg (m T : ℕ) : 0 ≤ self.N m T
• init (m : ℕ) : 1 ≤ m → self.N m 0 = 0
• step (m T : ℕ) : 1 ≤ m → self.N m (T + 1) ≤ self.N m T + ∑ j ∈ Finset.Ico 1 m, eps j m * self.N (m - j) T + E m * M

noncomputable def Lean4LPD.MultiLadder.majorant (eps : ℕ → ℕ → ℝ) (E : ℕ → ℝ) (M : ℝ) (m T : ℕ) : ℝ

The bound asserted by apd:eq:composition_majorant, as a function of the rung m and the number of layers T:

M · ∑_{k=0}^{T} C(T,k) · chain ε E k m.

In apd:eq:composition_majorant the outer sum is ∑_{k=1}^{min(m,T)}; the extra terms here vanish, at k = 0 by definition and at k > m by chain_eq_zero_of_lt. Summing to T rather than to min(m,T) is what makes the Pascal step below a two-line rewrite.

Equations

• Lean4LPD.MultiLadder.majorant eps E M m T = M * ∑ k ∈ Finset.range (T + 1), ↑(T.choose k) * Lean4LPD.chain eps E k m

theorem Lean4LPD.MultiLadder.sum_chain_succ {eps : ℕ → ℕ → ℝ} {E : ℕ → ℝ} (m T : ℕ) : ∑ k ∈ Finset.range (T + 2), ↑((T + 1).choose k) * chain eps E k m = ∑ k ∈ Finset.range (T + 1), ↑(T.choose k) * chain eps E k m + ∑ k ∈ Finset.range (T + 1), ↑(T.choose k) * chain eps E (k + 1) m

The Pascal recursion satisfied by the majorant's bracket, which is the whole content of the induction behind apd:eq:composition_majorant. Among the paths with k jumps in T layers, those whose final layer is idle are counted by C(T-1,k) and those that jump in the final layer by C(T-1,k-1); the two cases add up by Pascal's rule.

theorem Lean4LPD.MultiLadder.sum_chain_shift {eps : ℕ → ℕ → ℝ} {E : ℕ → ℝ} (m T : ℕ) : ∑ k ∈ Finset.range (T + 1), ↑(T.choose k) * chain eps E (k + 1) m = E m + ∑ j ∈ Finset.Ico 1 m, eps j m * ∑ k ∈ Finset.range (T + 1), ↑(T.choose k) * chain eps E k (m - j)

The shifted chain sum, unrolled one level: the k = 0 term is the entry factor E m, and every remaining term ends with a j-jump that starts from rung m - j.

theorem Lean4LPD.MultiLadder.le_majorant {M : ℝ} {eps : ℕ → ℕ → ℝ} {E : ℕ → ℝ} (L : MultiLadder eps E M) (heps : ∀ (j m : ℕ), 0 ≤ eps j m) (T m : ℕ) : 1 ≤ m → L.N m T ≤ majorant eps E M m T

The first-passage majorant. Formalizes apd:eq:composition_majorant:

N_m^{(T)} ≤ ‖O‖ · ∑_{k} C(T,k) · chain_k^{(m)}, chain_k^{(m)} = ∑_{0<ν₁<⋯<ν_k=m} E_{ν₁} ∏_{i=2}^{k} ε_{ν_i-ν_{i-1}}^{(ν_i)}.

The inner chain sum is chain, defined by peeling the last jump. Only nonnegativity of eps is needed; E and M are unconstrained, so the bound is inherited by any E majorizing the overshoot tail.

theorem Lean4LPD.MultiLadder.majorant_mono {M : ℝ} {eps : ℕ → ℕ → ℝ} {E : ℕ → ℝ} (heps : ∀ (j m : ℕ), 0 ≤ eps j m) (hE : ∀ (m : ℕ), 0 ≤ E m) (hM : 0 ≤ M) (m T : ℕ) : majorant eps E M m T ≤ majorant eps E M m (T + 1)

The majorant is monotone in the number of layers. This is what licenses bounding the rung norms at the intermediate layers of a Trotter step by the majorant taken at the last layer of the step. The rung norms themselves need not be monotone in the number of layers, so it is the majorant, not the norm, that is moved to the end of the step; see MultiLadder.block_inflow_le.

Non-vacuity

MultiLadder eps E M is inhabited whenever eps, E and M are nonnegative, so the theorems above are not statements about an empty type.

The witness below is the trivial one, N ≡ 0: it shows only that the field constraints are jointly satisfiable. It is not evidence that le_majorant is tight. For tightness, note that sum_chain_succ and sum_chain_shift combine to show that the majorant itself obeys the recursion of step with equality; that saturating family is not packaged as a MultiLadder here, and Lean4LPD.satLadder is the corresponding packaged statement on the single-jump side.

A Pauli instance of MultiLadder is constructed in Lean4LPD/Pauli/LayerLadder.lean (PauliString.pauliMultiLadder).

def Lean4LPD.MultiLadder.trivialMultiLadder {eps : ℕ → ℕ → ℝ} {E : ℕ → ℝ} {M : ℝ} (_heps : ∀ (j m : ℕ), 0 ≤ eps j m) (hE : ∀ (m : ℕ), 0 ≤ E m) (hM : 0 ≤ M) : MultiLadder eps E M

The zero family N ≡ 0 is a MultiLadder for all nonnegative eps, E and M.

Equations

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