Telescoping of the truncation error and the Pauli-norm triangle bound

This file formalizes the norm-level part of apd:thm:triangle for the step-boundary truncation of TrotterTruncate.lean. The difference between the untruncated evolution and the LPD output after r Trotter steps telescopes into the discarded operators X_{d+1} (apd:eq:step_component), each evolved through the remaining whole steps (trotterStep_telescoping). Conjugation by rotations with Hermitian Pauli generators preserves pauliNorm, so Minkowski's inequality in coefficient space bounds the error by the sum of the Pauli norms of the discarded operators (pauliNorm_trotterStep_error_le).

Main definitions

• blockEnd Gs θ period: one untruncated block of period rotations as an additive endomorphism of matrices; its r-th power is the untruncated evolution through r steps.

Main results

• pauliNorm_add_le, pauliNorm_sum_le: Minkowski's inequality for the Pauli 2-norm.
• trotterStep_telescoping, periodic_traj_sub_trotterStepTraj: the operator telescope, in terms of blockEnd and in terms of the rotation-indexed traj.
• blockEnd_pow_eq_periodic_traj: powers of blockEnd are traj of the rotations repeated modulo period.
• pauliNorm_trotterStep_error_le, pauliNorm_periodic_traj_error_le, pauliNorm_trotterTraj_error_le, pauliNorm_trotterStep_error_le_highNorm: the Pauli-norm triangle bound, for the three descriptions of the two trajectories and with the discarded norms written as high-weight norms.

Scope

pauliNorm is the normalized Hilbert–Schmidt (Pauli 2-) norm, not the matrix operator norm. The telescope needs no Hermiticity, locality, small-angle or entanglement hypothesis; the norm bound needs only Hermitian generators. The step of apd:thm:triangle that passes from Pauli norms to expectation values in a state, where the entanglement of the evolved state enters, is not formalized. The quantitative bound on the sum of the discarded norms is in LayerError.lean.

theorem Lean4LPD.PauliString.coeff_add {n : ℕ} (A B : Matrix (Bits n) (Bits n) ℂ) (p : PauliIndex n) : coeff (A + B) p = coeff A p + coeff B p

Coefficients are additive, the coefficient-space helper for the triangle inequality in apd:thm:triangle.

theorem Lean4LPD.PauliString.coeffVec_add {n : ℕ} (A B : Matrix (Bits n) (Bits n) ℂ) : coeffVec (A + B) = coeffVec A + coeffVec B

Coefficient vectors preserve addition, allowing the Pauli-norm form of the triangle step in apd:thm:triangle without choosing a norm instance on matrices.

@[simp]

theorem Lean4LPD.PauliString.pauliNorm_zero {n : ℕ} : pauliNorm 0 = 0

Zero contributes no error to the sum in apd:thm:triangle.

theorem Lean4LPD.PauliString.pauliNorm_add_le {n : ℕ} (A B : Matrix (Bits n) (Bits n) ℂ) : pauliNorm (A + B) ≤ pauliNorm A + pauliNorm B

Minkowski's inequality for the Pauli 2-norm, used on the operator telescope of apd:thm:triangle. This is an inequality for the ℓ² norm of the coefficient vector, not for the matrix operator norm.

theorem Lean4LPD.PauliString.pauliNorm_sum_le {n : ℕ} {ι : Type u_1} (S : Finset ι) (A : ι → Matrix (Bits n) (Bits n) ℂ) : pauliNorm (∑ i ∈ S, A i) ≤ ∑ i ∈ S, pauliNorm (A i)

Finite-sum Minkowski for the normalized Pauli norm, the norm-level triangle step associated with the operator telescope in apd:thm:triangle.

theorem Lean4LPD.PauliString.traj_add {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (A B : Matrix (Bits n) (Bits n) ℂ) (g : ℕ) : traj Gs θ (A + B) g = traj Gs θ A g + traj Gs θ B g

A block's untruncated evolution is additive. This is the linearity used by the telescope in apd:thm:triangle; the generators need not be Hermitian here.

theorem Lean4LPD.PauliString.traj_zero_input {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (g : ℕ) : traj Gs θ 0 g = 0

Zero remains zero under a whole untruncated block, the additive-map helper for apd:thm:triangle.

noncomputable def Lean4LPD.PauliString.blockEnd {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period : ℕ) : AddMonoid.End (Matrix (Bits n) (Bits n) ℂ)

A complete untruncated rotation block, as an additive endomorphism. Its powers represent the residual whole-step evolutions in apd:thm:triangle.

Equations

• Lean4LPD.PauliString.blockEnd Gs θ period = { toFun := fun (A : Matrix (Lean4LPD.Bits n) (Lean4LPD.Bits n) ℂ) => Lean4LPD.PauliString.traj Gs θ A period, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Lean4LPD.PauliString.blockEnd_apply {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period : ℕ) (A : Matrix (Bits n) (Bits n) ℂ) : (blockEnd Gs θ period) A = traj Gs θ A period

blockEnd applies the untruncated traj through one block, the evolution that appears in apd:eq:step_component.

theorem Lean4LPD.PauliString.trotterStep_telescoping {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (r : ℕ) : (blockEnd Gs θ period ^ r) O - trotterStepTraj Gs θ period wstar O r = ∑ d ∈ Finset.range r, (blockEnd Gs θ period ^ (r - 1 - d)) (discardedStep Gs θ period wstar O d)

The operator telescope. The identity of apd:thm:triangle: the untruncated evolution minus the LPD output after r steps is the sum of the discarded operators, each evolved through the remaining whole steps. Here discardedStep d is the zero-based X_{d+1} of apd:eq:step_component; its description as a high-weight projection is discardedStep_eq_truncOp. The proof is an induction on r that unfolds the definition of discardedStep; it needs no Hermiticity, locality or angle hypothesis.

theorem Lean4LPD.PauliString.traj_periodic_within_step {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (d i : ℕ) (hi : i ≤ period) : traj (fun (g : ℕ) => Gs (g % period)) (fun (g : ℕ) => θ (g % period)) O (d * period + i) = traj Gs θ (traj (fun (g : ℕ) => Gs (g % period)) (fun (g : ℕ) => θ (g % period)) O (d * period)) i

The untruncated, modulo-indexed run executes the specified block between successive boundaries, as used in apd:thm:triangle. The endpoint i = period is included. No positivity assumption is needed; period = 0 admits only i = 0.

theorem Lean4LPD.PauliString.blockEnd_pow_eq_periodic_traj {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (r : ℕ) : (blockEnd Gs θ period ^ r) O = traj (fun (g : ℕ) => Gs (g % period)) (fun (g : ℕ) => θ (g % period)) O (r * period)

The r-th power of the block evolution is the rotation-indexed untruncated traj at r * period, with the rotations repeated modulo period. This identifies the untruncated operator in apd:thm:triangle. It holds for every block length, including the empty block.

theorem Lean4LPD.PauliString.periodic_traj_sub_trotterStepTraj {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (r : ℕ) : traj (fun (g : ℕ) => Gs (g % period)) (fun (g : ℕ) => θ (g % period)) O (r * period) - trotterStepTraj Gs θ period wstar O r = ∑ d ∈ Finset.range r, traj (fun (g : ℕ) => Gs (g % period)) (fun (g : ℕ) => θ (g % period)) (discardedStep Gs θ period wstar O d) ((r - 1 - d) * period)

The operator telescope of apd:thm:triangle, entirely in terms of the rotation-indexed traj, the kept trajectory trotterStepTraj and the discarded operators discardedStep.

theorem Lean4LPD.PauliString.pauliNorm_blockEnd_pow {n : ℕ} {Gs : ℕ → PauliString n} (hG : ∀ (g : ℕ), IsSelfAdjoint (Gs g)) (θ : ℕ → ℝ) (period : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (r : ℕ) : pauliNorm ((blockEnd Gs θ period ^ r) O) = pauliNorm O

Evolution through whole blocks preserves the Pauli 2-norm, the invariance needed for the norm-level part of apd:thm:triangle. This is where Hermiticity of the generators is used.

theorem Lean4LPD.PauliString.pauliNorm_trotterStep_error_le {n : ℕ} {Gs : ℕ → PauliString n} (hG : ∀ (g : ℕ), IsSelfAdjoint (Gs g)) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (r : ℕ) : pauliNorm ((blockEnd Gs θ period ^ r) O - trotterStepTraj Gs θ period wstar O r) ≤ ∑ d ∈ Finset.range r, pauliNorm (discardedStep Gs θ period wstar O d)

The truncation error is bounded at Pauli-norm level. The operator telescope of apd:thm:triangle, Minkowski's inequality and invariance of the Pauli norm bound the error by the sum of the Pauli norms of the discarded operators X_{d+1} (apd:eq:step_component). This is the norm-level part of apd:thm:triangle; the passage to expectation values in a state is not formalized.

theorem Lean4LPD.PauliString.pauliNorm_periodic_traj_error_le {n : ℕ} {Gs : ℕ → PauliString n} (hG : ∀ (g : ℕ), IsSelfAdjoint (Gs g)) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (r : ℕ) : pauliNorm (traj (fun (g : ℕ) => Gs (g % period)) (fun (g : ℕ) => θ (g % period)) O (r * period) - trotterStepTraj Gs θ period wstar O r) ≤ ∑ d ∈ Finset.range r, pauliNorm (discardedStep Gs θ period wstar O d)

The Pauli-norm triangle bound of apd:thm:triangle with the untruncated side written as the rotation-indexed traj of the repeated block. The only hypothesis is Hermiticity of the generators.

theorem Lean4LPD.PauliString.pauliNorm_trotterTraj_error_le {n : ℕ} {Gs : ℕ → PauliString n} (hG : ∀ (g : ℕ), IsSelfAdjoint (Gs g)) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (r : ℕ) (hp : 0 < period) : pauliNorm (traj (fun (g : ℕ) => Gs (g % period)) (fun (g : ℕ) => θ (g % period)) O (r * period) - trotterTraj Gs θ period wstar O (r * period)) ≤ ∑ d ∈ Finset.range r, pauliNorm (discardedStep Gs θ period wstar O d)

The norm-level error bound of apd:thm:triangle for the rotation-indexed execution trotterTraj with cuts at step boundaries. Positive block length is needed only to identify this scheduled trajectory with the step-indexed recurrence trotterStepTraj.

theorem Lean4LPD.PauliString.pauliNorm_trotterStep_error_le_highNorm {n : ℕ} {Gs : ℕ → PauliString n} (hG : ∀ (g : ℕ), IsSelfAdjoint (Gs g)) (θ : ℕ → ℝ) (period wstar : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) (r : ℕ) : pauliNorm ((blockEnd Gs θ period ^ r) O - trotterStepTraj Gs θ period wstar O r) ≤ ∑ d ∈ Finset.range r, highNorm wstar (traj Gs θ (trotterStepTraj Gs θ period wstar O d) period)

The norm-level triangle bound with the discarded norms written as the high-weight norms of the operators before truncation, as in the last equality of apd:thm:triangle. These are not the high-weight norms of the kept operators, which vanish.