The Pauli coefficient vector, and ‖O‖_{2,normalized} = ‖x‖_{ℓ²}

This file sets up the coefficient-vector picture in which the proof of apd:thm:local_flow_k_local takes place. An operator O on n qubits has Pauli coefficients x_P = 2^{-n} Tr(P O), indexed by the 4^n Pauli strings of def:pauli_basis. Those strings are orthonormal for the normalized Hilbert–Schmidt inner product ⟨A,B⟩ := 2^{-n} Tr(A† B), so the normalized Schatten 2-norm ‖O‖_{2,normalized} (the Pauli 2-norm) equals the ℓ² norm of the coefficient vector. The high-weight norm of apd:eq:def_high_weight_norm is then the ℓ² norm of the coefficient vector restricted to the classes above a weight threshold.

Main definitions

• PauliIndex n: the signless Pauli classes (x, z), the index set of the expansion.
• PauliString.cls, PauliString.herm: the class of a Pauli string, and the self-adjoint representative of a class.
• PauliString.wt: the weight of a class (def:pauli_weight).
• PauliString.coeff, PauliString.coeffVec: the coefficient x_P, and the coefficient vector as an element of EuclideanSpace ℂ (PauliIndex n).
• PauliString.pauliNormSq, PauliString.pauliNorm: the Pauli 2-norm, defined entrywise.
• PauliString.restr: restriction of a coefficient vector to a set of classes.
• PauliString.highSet, PauliString.highNorm: the region {p : w < |p|} and the high-weight norm ‖O_{≥ w+1}‖_{2,normalized} (apd:eq:def_high_weight_norm).

Main results

• PauliString.pauliNormSq_eq_trace: ‖O‖_{2,normalized}² = 2^{-n} Tr(O† O).
• PauliString.sum_norm_coeff_sq, PauliString.norm_coeffVec: Parseval, ‖x‖_{ℓ²} = ‖O‖_{2,normalized}.
• PauliString.coeff_toMatrix_herm: the coefficient vector of a basis Pauli is a unit vector.
• PauliString.highNorm_le_pauliNorm, PauliString.highNorm_eq_zero, PauliString.highNorm_pos_of_coeff_ne_zero: the basic facts about the high-weight norm.

The normalization

The expansion is in the unnormalized strings {I,X,Y,Z}^{⊗n}, with the factor 2^{-n} carried by the coefficient. They are orthonormal for ⟨·,·⟩ because Tr(P† P) = 2^n (trace_star_toMatrix_mul_self), which is why no further constant appears in Parseval.

The index set, and the phase that has to be chosen

Pauli/Trace.lean proves that the trace pairing sees only the (x, z) data, so the phase-extended Pauli group is not an orthogonal family. The index set of the expansion therefore cannot be PauliString n; it is the 4^n signless classes PauliIndex n := Bits n × Bits n, and a representative has to be chosen in each. herm chooses the self-adjoint one with phase (z ⬝ᵥ x).val ∈ {0, 1}.

Self-adjointness is the only part of the choice that matters downstream: isSelfAdjoint_iff_phase pins the phase's parity and leaves a sign, and herm_eq_or_eq_neg records that a different admissible choice changes herm p only by ±1. Nothing here needs the finer convention phase = #{Y-sites} mod 4, which identifies the representative with the tensor product of the one-qubit matrices I, X, Y, Z with coefficient +1; Pauli/Tensor.lean makes that comparison.

The coefficients are not proved real. coeff O p : ℂ. For a self-adjoint O every coefficient is real, since the representatives are self-adjoint, but that lemma is neither proved nor needed: the flow argument works verbatim over ℂ because the transformation is by real planar rotations, so Pauli/Flow.lean never asks. The real coefficient vector of the paper's proof is therefore mirrored in the operators (self-adjoint representatives), not in the scalars.

Parseval, without a basis

sum_norm_coeff_sq is the identity ‖x‖_{ℓ²}² = ‖O‖_{2,normalized}², and it is proved by a direct character sum, not by exhibiting an orthonormal basis. The reason is economy: the basis route needs linear independence, a finrank count for Matrix (Bits n) (Bits n) ℂ, and an InnerProductSpace instance on matrices; the direct route needs char_sum, which Pauli/Trace.lean already has. In one line: for a fixed x-part, Tr(P_{x,z} O) is the z-character transform of the shifted diagonal b ↦ O_{b, b+x} (trace_toMatrix_mul), and Plancherel for (ZMod 2)^n turns the sum over z into 2^n times the sum of |O_{b,b+x}|². Summing over x sweeps every entry of O exactly once.

Parseval alone does not give completeness, O = ∑_P x_P P. That is proved in Pauli/Truncate.lean, as truncOp_univ and sum_coeff_smul_toMatrix_herm, from Parseval and the reproducing property coeff_truncOp: an operator whose coefficients all vanish has ‖·‖_{2,normalized} = 0 and hence vanishing entries. Neither a finrank count nor an InnerProductSpace instance is needed for it.

@[simp]

theorem Lean4LPD.norm_iPow (k : ZMod 4) : ‖iPow k‖ = 1

Fourth roots of unity have modulus one.

@[reducible, inline]

abbrev Lean4LPD.PauliIndex (n : ℕ) : Type

The signless Pauli class: the (x, z) data of a Pauli string, with the phase forgotten. There are 4^n of them, and they — not the 4·4^n group elements — index the Pauli basis of def:pauli_basis.

Equations

• Lean4LPD.PauliIndex n = (Lean4LPD.Bits n × Lean4LPD.Bits n)

Classes and their Hermitian representatives

def Lean4LPD.PauliString.cls {n : ℕ} (s : PauliString n) : PauliIndex n

The class of a Pauli string.

Equations

• s.cls = (s.x, s.z)

@[simp]

theorem Lean4LPD.PauliString.cls_fst {n : ℕ} (s : PauliString n) : s.cls.1 = s.x

@[simp]

theorem Lean4LPD.PauliString.cls_snd {n : ℕ} (s : PauliString n) : s.cls.2 = s.z

def Lean4LPD.PauliString.herm {n : ℕ} (p : PauliIndex n) : PauliString n

The self-adjoint representative of a class, i^{z ⬝ᵥ x} X^x Z^z. Defined, not characterized: isSelfAdjoint_iff_phase admits two phases differing by 2, and this picks the one in {0, 1}. See herm_eq_or_eq_neg for what the other choice would cost.

Equations

• Lean4LPD.PauliString.herm p = { x := p.1, z := p.2, phase := ↑(p.2 ⬝ᵥ p.1).val }

@[simp]

theorem Lean4LPD.PauliString.herm_x {n : ℕ} (p : PauliIndex n) : (herm p).x = p.1

@[simp]

theorem Lean4LPD.PauliString.herm_z {n : ℕ} (p : PauliIndex n) : (herm p).z = p.2

@[simp]

theorem Lean4LPD.PauliString.cls_herm {n : ℕ} (p : PauliIndex n) : (herm p).cls = p

theorem Lean4LPD.PauliString.isSelfAdjoint_herm {n : ℕ} (p : PauliIndex n) : IsSelfAdjoint (herm p)

herm p is self-adjoint, so toMatrix (herm p) is a Hermitian operator.

theorem Lean4LPD.PauliString.phase_sub_of_isSelfAdjoint {n : ℕ} {s t : PauliString n} (hs : IsSelfAdjoint s) (ht : IsSelfAdjoint t) (hx : s.x = t.x) (hz : s.z = t.z) : s.phase - t.phase = 0 ∨ s.phase - t.phase = 2

Two self-adjoint Pauli strings on the same class differ by at most a sign: their phases differ by 0 or 2. This is the residual freedom isSelfAdjoint_iff_phase leaves.

theorem Lean4LPD.PauliString.herm_eq_or_eq_neg {n : ℕ} {s : PauliString n} (hs : IsSelfAdjoint s) : s = herm s.cls ∨ s = phaseMul 2 (herm s.cls)

Any self-adjoint representative of a class is ± herm.

The weight of a class

theorem Lean4LPD.PauliString.weight_congr {n : ℕ} {s t : PauliString n} (hx : s.x = t.x) (hz : s.z = t.z) : s.weight = t.weight

The weight sees only the (x, z) data.

def Lean4LPD.PauliString.wt {n : ℕ} (p : PauliIndex n) : ℕ

The weight of a Pauli class, def:pauli_weight transported to the index set. Well defined because the weight cannot see a phase.

Equations

• Lean4LPD.PauliString.wt p = (Lean4LPD.PauliString.herm p).weight

@[simp]

theorem Lean4LPD.PauliString.wt_cls {n : ℕ} (s : PauliString n) : wt s.cls = s.weight

The coefficient vector

noncomputable def Lean4LPD.PauliString.coeff {n : ℕ} (O : Matrix (Bits n) (Bits n) ℂ) (p : PauliIndex n) : ℂ

The Pauli coefficient vector x_P = 2^{-n} Tr(P O), with P the self-adjoint representative of the class p.

Equations

• Lean4LPD.PauliString.coeff O p = (2 ^ n)⁻¹ * ((Lean4LPD.PauliString.herm p).toMatrix * O).trace

noncomputable def Lean4LPD.PauliString.pauliNormSq {n : ℕ} (O : Matrix (Bits n) (Bits n) ℂ) : ℝ

The squared Pauli 2-norm ‖O‖_{2,normalized}² = 2^{-n} Tr(O† O), written entrywise as 2^{-n} ∑_{a,b} |O_{ab}|². pauliNormSq_eq_trace is the equality with the trace form.

Equations

• Lean4LPD.PauliString.pauliNormSq O = (2 ^ n)⁻¹ * ∑ a : Lean4LPD.Bits n, ∑ b : Lean4LPD.Bits n, ‖O a b‖ ^ 2

noncomputable def Lean4LPD.PauliString.pauliNorm {n : ℕ} (O : Matrix (Bits n) (Bits n) ℂ) : ℝ

The Pauli 2-norm ‖O‖_{2,normalized}, the normalized Schatten 2-norm: ‖O‖_{2,normalized}² = 2^{-n} Tr(O† O), so that every Pauli string has norm one. This is the norm in which the high-weight norm of apd:eq:def_high_weight_norm is measured.

Equations

• Lean4LPD.PauliString.pauliNorm O = √(Lean4LPD.PauliString.pauliNormSq O)

theorem Lean4LPD.PauliString.pauliNormSq_nonneg {n : ℕ} (O : Matrix (Bits n) (Bits n) ℂ) : 0 ≤ pauliNormSq O

theorem Lean4LPD.PauliString.pauliNorm_nonneg {n : ℕ} (O : Matrix (Bits n) (Bits n) ℂ) : 0 ≤ pauliNorm O

@[simp]

theorem Lean4LPD.PauliString.pauliNorm_sq {n : ℕ} (O : Matrix (Bits n) (Bits n) ℂ) : pauliNorm O ^ 2 = pauliNormSq O

theorem Lean4LPD.PauliString.pauliNormSq_eq_trace {n : ℕ} (O : Matrix (Bits n) (Bits n) ℂ) : ↑(pauliNormSq O) = (2 ^ n)⁻¹ * (star O * O).trace

‖O‖_{2,normalized}² = 2^{-n} Tr(O† O): the entrywise definition pauliNormSq agrees with the trace form of the normalized Schatten 2-norm.

The trace against a Pauli, as a character transform

theorem Lean4LPD.PauliString.trace_toMatrix_mul {n : ℕ} (s : PauliString n) (O : Matrix (Bits n) (Bits n) ℂ) : (s.toMatrix * O).trace = iPow s.phase * ∑ b : Bits n, negOnePow (s.z ⬝ᵥ b) * O b (b + s.x)

Tr(s O) is a character transform of a shifted diagonal of O. The matrix toMatrix s is monomial, so the double sum of the trace collapses to a single one: the X-part s.x selects which off-diagonal of O is read, and the Z-part s.z supplies the character.

Parseval

Plancherel for (ZMod 2)^n, then a sweep over the X-parts.

theorem Lean4LPD.PauliString.sum_norm_coeff_sq {n : ℕ} (O : Matrix (Bits n) (Bits n) ℂ) : ∑ p : PauliIndex n, ‖coeff O p‖ ^ 2 = pauliNormSq O

Parseval: ‖O‖_{2,normalized} = ‖x‖_{ℓ²}, squared. This is the identity the proof of apd:thm:local_flow_k_local starts from; it expresses the orthonormality of the Pauli strings for ⟨A,B⟩ = 2^{-n} Tr(A† B).

Proved directly from the character sum rather than through an orthonormal basis, so it does not by itself give the expansion O = ∑_P x_P P; that is sum_coeff_smul_toMatrix_herm in Pauli/Truncate.lean.

theorem Lean4LPD.PauliString.pauliNorm_eq_sqrt_sum {n : ℕ} (O : Matrix (Bits n) (Bits n) ℂ) : pauliNorm O = √(∑ p : PauliIndex n, ‖coeff O p‖ ^ 2)

‖O‖_{2,normalized} = ‖x‖_{ℓ²}, as norms rather than squares.

The coefficients of a single Pauli

A guard against a vacuous reading of everything above, and the cheapest consequence of Pauli/Trace.lean's orthogonality: the coefficient vector of one basis Pauli is the corresponding unit vector. This is what makes the locality hypothesis of highNorm_eq_zero (no coefficient above a given weight, cf. def:support) satisfiable by a concrete observable.

theorem Lean4LPD.PauliString.coeff_toMatrix_herm {n : ℕ} (p q : PauliIndex n) : coeff (herm q).toMatrix p = if p = q then 1 else 0

The coefficient vector of a basis Pauli is a unit vector.

theorem Lean4LPD.PauliString.coeff_toMatrix_herm_eq_zero {n : ℕ} {p q : PauliIndex n} (h : wt q < wt p) : coeff (herm q).toMatrix p = 0

A basis Pauli is |q|-local: no class of larger weight carries a coefficient.

The coefficient vector as an ℓ² vector, and its weight-graded pieces

The proof of apd:thm:local_flow_k_local treats the coefficients as an ℓ² vector and applies Minkowski's inequality on that space, so the coefficients are packaged as an element of EuclideanSpace ℂ (PauliIndex n). That buys the triangle inequality; nothing else here needs the inner product.

noncomputable def Lean4LPD.PauliString.coeffVec {n : ℕ} (O : Matrix (Bits n) (Bits n) ℂ) : EuclideanSpace ℂ (PauliIndex n)

The coefficient vector x = (x_P)_P of an operator, as a vector in ℓ²(PauliIndex n).

Equations

• Lean4LPD.PauliString.coeffVec O = WithLp.toLp 2 (Lean4LPD.PauliString.coeff O)

@[simp]

theorem Lean4LPD.PauliString.coeffVec_apply {n : ℕ} (O : Matrix (Bits n) (Bits n) ℂ) (p : PauliIndex n) : (coeffVec O).ofLp p = coeff O p

theorem Lean4LPD.PauliString.norm_coeffVec {n : ℕ} (O : Matrix (Bits n) (Bits n) ℂ) : ‖coeffVec O‖ = pauliNorm O

‖O‖_{2,normalized} = ‖x‖_{ℓ²}, as an identity of norms: the Pauli 2-norm of the operator is the ℓ² norm of its coefficient vector.

noncomputable def Lean4LPD.PauliString.restr {n : ℕ} (S : Finset (PauliIndex n)) (y : EuclideanSpace ℂ (PauliIndex n)) : EuclideanSpace ℂ (PauliIndex n)

Restriction of a coefficient vector to a set of classes S, zeroing every other coefficient. For S the high-weight region this is the block x_R of the splitting x = x_R + x_B used in the proof of apd:thm:local_flow_k_local; for its complement it is the coefficient side of the truncation Π_{≤ w} (see truncOp in Pauli/Truncate.lean).

Equations

• Lean4LPD.PauliString.restr S y = WithLp.toLp 2 fun (p : Lean4LPD.PauliIndex n) => if p ∈ S then y.ofLp p else 0

@[simp]

theorem Lean4LPD.PauliString.restr_apply {n : ℕ} (S : Finset (PauliIndex n)) (y : EuclideanSpace ℂ (PauliIndex n)) (p : PauliIndex n) : (restr S y).ofLp p = if p ∈ S then y.ofLp p else 0

theorem Lean4LPD.PauliString.norm_restr_sq {n : ℕ} (S : Finset (PauliIndex n)) (y : EuclideanSpace ℂ (PauliIndex n)) : ‖restr S y‖ ^ 2 = ∑ p ∈ S, ‖y.ofLp p‖ ^ 2

theorem Lean4LPD.PauliString.norm_restr_le {n : ℕ} (S : Finset (PauliIndex n)) (y : EuclideanSpace ℂ (PauliIndex n)) : ‖restr S y‖ ≤ ‖y‖

Dropping classes cannot increase the ℓ² mass.

@[simp]

theorem Lean4LPD.PauliString.restr_univ {n : ℕ} (y : EuclideanSpace ℂ (PauliIndex n)) : restr Finset.univ y = y

theorem Lean4LPD.PauliString.restr_add {n : ℕ} (S : Finset (PauliIndex n)) (y z : EuclideanSpace ℂ (PauliIndex n)) : restr S (y + z) = restr S y + restr S z

theorem Lean4LPD.PauliString.restr_add_restr_compl {n : ℕ} (S : Finset (PauliIndex n)) (y : EuclideanSpace ℂ (PauliIndex n)) : restr S y + restr Sᶜ y = y

x = x_R + x_B: a coefficient vector is the sum of its restrictions to a set of classes and to the complement.

The high-weight region

def Lean4LPD.PauliString.highSet (n w : ℕ) : Finset (PauliIndex n)

The high-weight region R = {p : |p| > w}: the classes of weight above the threshold w.

Equations

• Lean4LPD.PauliString.highSet n w = {p : Lean4LPD.PauliIndex n | w < Lean4LPD.PauliString.wt p}

@[simp]

theorem Lean4LPD.PauliString.mem_highSet {n w : ℕ} {p : PauliIndex n} : p ∈ highSet n w ↔ w < wt p

noncomputable def Lean4LPD.PauliString.highNorm {n : ℕ} (w : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) : ℝ

The high-weight norm ‖O_{≥ w+1}‖_{2,normalized} of apd:eq:def_high_weight_norm, at threshold w: the ℓ² mass of the coefficients on classes of weight > w.

Equations

• Lean4LPD.PauliString.highNorm w O = ‖Lean4LPD.PauliString.restr (Lean4LPD.PauliString.highSet n w) (Lean4LPD.PauliString.coeffVec O)‖

theorem Lean4LPD.PauliString.highNorm_nonneg {n : ℕ} (w : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) : 0 ≤ highNorm w O

theorem Lean4LPD.PauliString.highNorm_le_pauliNorm {n : ℕ} (w : ℕ) (O : Matrix (Bits n) (Bits n) ℂ) : highNorm w O ≤ pauliNorm O

The high-weight mass never exceeds the total mass: ‖O_{≥ w+1}‖_{2,normalized} ≤ ‖O‖_{2,normalized} at every threshold w. This is the inequality behind the base case of the induction in apd:cor:norm_cumulation_jump.

theorem Lean4LPD.PauliString.highNorm_eq_zero {n : ℕ} (w : ℕ) {O : Matrix (Bits n) (Bits n) ℂ} (h : ∀ (p : PauliIndex n), w < wt p → coeff O p = 0) : highNorm w O = 0

A k_o-local observable has no mass above weight k_o: init for the ladder. Locality is read through the coefficient vector (cf. def:support): every class carrying a non-zero coefficient has weight at most w.

theorem Lean4LPD.PauliString.highNorm_pos_of_coeff_ne_zero {n w : ℕ} {O : Matrix (Bits n) (Bits n) ℂ} {p : PauliIndex n} (hp : w < wt p) (h : coeff O p ≠ 0) : 0 < highNorm w O

The converse of highNorm_eq_zero: a single nonzero coefficient above the cut forces positive high-weight mass. Used wherever a witness must show the discarded sector is really occupied rather than merely reachable.