The j-jump decomposition of a Pauli layer and the layer-inflow bound

This file formalizes apd:thm:layer_inflow. For a finite ordered list L of Pauli rotations (G, θ), the coefficient action layerAct L of the matrix conjugation layerConj L is expanded by the number j of sine branches taken, layerAct L = ∑ j, layerJump L j. If the generators have pairwise disjoint supports and weight at most k_h (IsLayer), then the block layerInflowMatrix L w j of the exactly-j component that maps Pauli weights ≤ w to Pauli weights > w has ℓ² operator norm at most

C(w + j (k_h - 1), j) σ^j ≤ ((w + j (k_h - 1)) σ)^j / j! (apd:eq:layer_inflow),

where σ is any bound on |sin θ| over the layer. The norm bound is the Schur test Lean4LPD.l2_opNorm_le_of_row_col_bound applied to absolute row and column sums.

Main definitions

• stayAct, jumpAct: the cosine/identity branch and the sine branch of a single rotation; they add up to rotAct (rotAct_eq_stay_add_jump).
• layerAct, layerConj: a finite ordered layer as a map on coefficient vectors and as matrix conjugation, related by coeffVec_layerConj.
• layerJump L j: the component of layerAct L with exactly j sine branches.
• antiLayer L p, layerAntiCount L p: the generators of L that anticommute with the Pauli p, as a finset and as a count with list multiplicity.
• layerSigma L: the largest |sin θ| in the layer.
• layerJumpMatrix L j, layerInflowMatrix L w j: the matrix of layerJump L j and its high-from-low block A^{(j)}.

Main results

• layerAct_eq_sum_layerJump: the finite expansion of a layer by number of sine branches.
• layerJump_apply_eq_zero_of_weight_lt: j sine branches raise the Pauli weight by at most j (k_h - 1).
• card_antiLayer_le_weight: in a disjoint-support layer at most |p| generators anticommute with p.
• row_sum_norm_layerJumpMatrix_le, col_sum_norm_layerJumpMatrix_le: binomial bounds on the absolute row and column sums of layerJumpMatrix L j.
• norm_layerInflowMatrix_le, norm_layerInflowMatrix_le_factorial, norm_layerInflowMatrix_le_layerSigma: the layer-inflow bound in binomial form, in factorial form, and with σ = layerSigma L.
• restr_layerAct_low_eq_sum_inflow, norm_restr_layerAct_le_sum_inflow: on low-weight inputs the high-weight part of the layer output is ∑ j, A^{(j)}, and the high-weight norm after a layer is at most the high-weight norm before it plus the norms of the inflows.
• layerInflowMatrix_clm_restr, norm_layerInflowMatrix_clm_le_restr: a j-jump inflow into weights above w only sees input weights above w' whenever w' + j (k_h - 1) ≤ w, the form needed for apd:rmk:multijump.

Implementation notes

The layer action is built from the conjugation action rotAct of Flow.lean, so every statement is about the Pauli coefficients of layerConj L O. The expansion and the weight bound hold for arbitrary ordered lists. The row and column estimates need only pairwise commutation of the generators; disjointness of supports enters when the number of anticommuting generators is bounded by the Pauli weight. The row and column sums are bounded by induction on the list, using Pascal's rule and the fact that a rotation whose generator commutes with G preserves the commutation class with G. Distinct branch choices are not claimed to give distinct nonzero matrix entries: cancellations are allowed, and only upper bounds are asserted.

The small parameter is a bound σ on the absolute sines, so the angles are arbitrary real numbers. This is more general than the paper's statement: neither positivity of the sines nor monotonicity of sine on an interval of angles is used.

No MultiLadder is constructed here; the passage from the finite inflow sum to the recurrence with the infinite entry factor is in LayerLadder.lean.

noncomputable def Lean4LPD.PauliString.stayAct {n : ℕ} (G : PauliString n) (θ : ℝ) (y : EuclideanSpace ℂ (PauliIndex n)) : EuclideanSpace ℂ (PauliIndex n)

The unchanged branch of a rotation: identity on commuting coordinates and cosine on anticommuting coordinates (apd:thm:layer_inflow).

Equations

• G.stayAct θ y = WithLp.toLp 2 fun (p : Lean4LPD.PauliIndex n) => if G.sympForm (Lean4LPD.PauliString.herm p) = 0 then y.ofLp p else ↑(Real.cos θ) * y.ofLp p

noncomputable def Lean4LPD.PauliString.jumpAct {n : ℕ} (G : PauliString n) (θ : ℝ) (y : EuclideanSpace ℂ (PauliIndex n)) : EuclideanSpace ℂ (PauliIndex n)

The sine branch, with the coefficient-side partner sign fixed by coeffVec_conj. Supporting definition for apd:thm:layer_inflow.

Equations

• G.jumpAct θ y = WithLp.toLp 2 fun (p : Lean4LPD.PauliIndex n) => if G.sympForm (Lean4LPD.PauliString.herm p) = 0 then 0 else -↑(Real.sin θ) * (G.partnerSign p * y.ofLp (G.partner p))

@[simp]

theorem Lean4LPD.PauliString.stayAct_apply {n : ℕ} (G : PauliString n) (θ : ℝ) (y : EuclideanSpace ℂ (PauliIndex n)) (p : PauliIndex n) : (G.stayAct θ y).ofLp p = if G.sympForm (herm p) = 0 then y.ofLp p else ↑(Real.cos θ) * y.ofLp p

Coefficient formula for the unchanged branch; supporting lemma for apd:thm:layer_inflow.

@[simp]

theorem Lean4LPD.PauliString.jumpAct_apply {n : ℕ} (G : PauliString n) (θ : ℝ) (y : EuclideanSpace ℂ (PauliIndex n)) (p : PauliIndex n) : (G.jumpAct θ y).ofLp p = if G.sympForm (herm p) = 0 then 0 else -↑(Real.sin θ) * (G.partnerSign p * y.ofLp (G.partner p))

Coefficient formula for the sine branch; supporting lemma for apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.rotAct_eq_stay_add_jump {n : ℕ} (G : PauliString n) (θ : ℝ) (y : EuclideanSpace ℂ (PauliIndex n)) : G.rotAct θ y = G.stayAct θ y + G.jumpAct θ y

The two branches add up to the rotation action rotAct, which coeffVec_conj identifies with conjugation by the rotation. Supporting lemma for apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.stayAct_add {n : ℕ} (G : PauliString n) (θ : ℝ) (y z : EuclideanSpace ℂ (PauliIndex n)) : G.stayAct θ (y + z) = G.stayAct θ y + G.stayAct θ z

Additivity of the unchanged branch, supporting finite expansion in apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.jumpAct_add {n : ℕ} (G : PauliString n) (θ : ℝ) (y z : EuclideanSpace ℂ (PauliIndex n)) : G.jumpAct θ (y + z) = G.jumpAct θ y + G.jumpAct θ z

Additivity of the sine branch, supporting finite expansion in apd:thm:layer_inflow.

@[simp]

theorem Lean4LPD.PauliString.stayAct_zero {n : ℕ} (G : PauliString n) (θ : ℝ) : G.stayAct θ 0 = 0

Zero is preserved by the unchanged branch; supporting lemma for apd:thm:layer_inflow.

@[simp]

theorem Lean4LPD.PauliString.jumpAct_zero {n : ℕ} (G : PauliString n) (θ : ℝ) : G.jumpAct θ 0 = 0

Zero is preserved by the sine branch; supporting lemma for apd:thm:layer_inflow.

noncomputable def Lean4LPD.PauliString.layerAct {n : ℕ} : List (PauliString n × ℝ) → EuclideanSpace ℂ (PauliIndex n) → EuclideanSpace ℂ (PauliIndex n)

Coefficient action of a finite ordered list of rotations, the composition of their rotAct (the head of the list acts last). For disjoint supports this is the layer of apd:thm:layer_inflow.

Equations

• Lean4LPD.PauliString.layerAct [] x✝ = x✝
• Lean4LPD.PauliString.layerAct ((G, θ) :: L) x✝ = G.rotAct θ (Lean4LPD.PauliString.layerAct L x✝)

noncomputable def Lean4LPD.PauliString.layerConj {n : ℕ} : List (PauliString n × ℝ) → Matrix (Bits n) (Bits n) ℂ → Matrix (Bits n) (Bits n) ℂ

Matrix conjugation by the rotations of a list, in the same order as layerAct. It is defined from the rotation matrices rot, independently of the branch expansion (apd:thm:layer_inflow).

Equations

• Lean4LPD.PauliString.layerConj [] x✝ = x✝
• Lean4LPD.PauliString.layerConj ((G, θ) :: L) x✝ = Lean4LPD.rot G.toMatrix θ * Lean4LPD.PauliString.layerConj L x✝ * Lean4LPD.rot G.toMatrix (-θ)

theorem Lean4LPD.PauliString.coeffVec_layerConj {n : ℕ} (L : List (PauliString n × ℝ)) (hL : ∀ g ∈ L, IsSelfAdjoint g.1) (O : Matrix (Bits n) (Bits n) ℂ) : coeffVec (layerConj L O) = layerAct L (coeffVec O)

For Hermitian generators, layerAct L is the action of the matrix conjugation layerConj L on coefficient vectors. Supporting lemma for apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.norm_layerAct {n : ℕ} (L : List (PauliString n × ℝ)) (hL : ∀ g ∈ L, IsSelfAdjoint g.1) (y : EuclideanSpace ℂ (PauliIndex n)) : ‖layerAct L y‖ = ‖y‖

A finite layer of Hermitian generators preserves the coefficient ℓ² norm. This gives the contraction of the diagonal (high-to-high) block; the off-diagonal block is handled by the Schur bound of apd:thm:layer_inflow below.

noncomputable def Lean4LPD.PauliString.layerJump {n : ℕ} : List (PauliString n × ℝ) → ℕ → EuclideanSpace ℂ (PauliIndex n) → EuclideanSpace ℂ (PauliIndex n)

The component of layerAct L in which exactly j rotations take their sine branch, defined by recursion on the list: the head rotation either stays, or takes its sine branch and leaves j - 1 sine branches to the tail. Rotations that stay keep their cosine or identity factor. Supporting definition for A^{(j)} in apd:thm:layer_inflow.

Equations

• Lean4LPD.PauliString.layerJump [] 0 x✝ = x✝
• Lean4LPD.PauliString.layerJump [] n_1.succ x✝ = 0
• Lean4LPD.PauliString.layerJump ((G, θ) :: L) 0 x✝ = G.stayAct θ (Lean4LPD.PauliString.layerJump L 0 x✝)
• Lean4LPD.PauliString.layerJump ((G, θ) :: L) j.succ x✝ = G.stayAct θ (Lean4LPD.PauliString.layerJump L (j + 1) x✝) + G.jumpAct θ (Lean4LPD.PauliString.layerJump L j x✝)

theorem Lean4LPD.PauliString.layerJump_eq_zero_of_length_lt {n : ℕ} (L : List (PauliString n × ℝ)) (j : ℕ) (hj : L.length < j) (y : EuclideanSpace ℂ (PauliIndex n)) : layerJump L j y = 0

A layer cannot take more sine branches than it has rotations. Supporting lemma for the finite form of apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.stayAct_sum {n : ℕ} {ι : Type u_1} (s : Finset ι) (G : PauliString n) (θ : ℝ) (f : ι → EuclideanSpace ℂ (PauliIndex n)) : G.stayAct θ (∑ i ∈ s, f i) = ∑ i ∈ s, G.stayAct θ (f i)

The unchanged branch distributes over finite coefficient sums; supporting lemma for apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.jumpAct_sum {n : ℕ} {ι : Type u_1} (s : Finset ι) (G : PauliString n) (θ : ℝ) (f : ι → EuclideanSpace ℂ (PauliIndex n)) : G.jumpAct θ (∑ i ∈ s, f i) = ∑ i ∈ s, G.jumpAct θ (f i)

The sine branch distributes over finite coefficient sums; supporting lemma for apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.layerAct_eq_sum_layerJump {n : ℕ} (L : List (PauliString n × ℝ)) (y : EuclideanSpace ℂ (PauliIndex n)) : layerAct L y = ∑ j ∈ Finset.range (L.length + 1), layerJump L j y

Expansion of a layer by number of sine branches. layerAct L is the finite sum of its exactly-j components, 0 ≤ j ≤ L.length; this is the expansion used in apd:thm:layer_inflow. It is an identity for arbitrary ordered lists of rotations: disjointness and commutation are needed only for the binomial counting estimates below.

theorem Lean4LPD.PauliString.stayAct_apply_eq_zero {n : ℕ} (G : PauliString n) (θ : ℝ) (y : EuclideanSpace ℂ (PauliIndex n)) (p : PauliIndex n) (hy : y.ofLp p = 0) : (G.stayAct θ y).ofLp p = 0

A zero input coordinate stays zero in the unchanged branch; supporting lemma for apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.layerJump_apply_eq_zero_of_weight_lt {n : ℕ} (L : List (PauliString n × ℝ)) {kh w : ℕ} (hk : ∀ g ∈ L, g.1.weight ≤ kh) (y : EuclideanSpace ℂ (PauliIndex n)) (hy : ∀ (p : PauliIndex n), w < wt p → y.ofLp p = 0) (j : ℕ) (p : PauliIndex n) (hp : w + j * (kh - 1) < wt p) : (layerJump L j y).ofLp p = 0

Exactly j sine branches raise the Pauli weight by at most j (k_h - 1). If the input has no coefficient above weight w, then layerJump L j of it has none above w + j (k_h - 1); this is the weight bookkeeping of apd:thm:layer_inflow. Cancellations can remove coefficients, so only support containment is asserted. No disjointness is needed.

theorem Lean4LPD.PauliString.layerJump_single_eq_zero_of_weight_lt {n : ℕ} (L : List (PauliString n × ℝ)) {kh : ℕ} (hk : ∀ g ∈ L, g.1.weight ≤ kh) (j : ℕ) (p q : PauliIndex n) (hp : wt q + j * (kh - 1) < wt p) : (layerJump L j (WithLp.toLp 2 (Pi.single q 1))).ofLp p = 0

Finite-support transfer in a j-branch matrix column: the input basis vector at q can reach only coordinates of weight at most wt q + j(k_h-1). Supporting lemma for the row bound of apd:thm:layer_inflow.

def Lean4LPD.PauliString.antiLayer {n : ℕ} (L : List (PauliString n)) (p : PauliIndex n) : Finset (PauliString n)

The set 𝒜(p) of generators of a finite layer that anticommute with the Pauli p. Supporting definition for apd:thm:layer_inflow.

Equations

• Lean4LPD.PauliString.antiLayer L p = {G ∈ L.toFinset | G.sympForm (Lean4LPD.PauliString.herm p) = 1}

@[simp]

theorem Lean4LPD.PauliString.mem_antiLayer {n : ℕ} (L : List (PauliString n)) (p : PauliIndex n) (G : PauliString n) : G ∈ antiLayer L p ↔ G ∈ L ∧ G.sympForm (herm p) = 1

Membership in the layer's anticommuting generator set; supporting lemma for apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.card_antiLayer_le_weight {n : ℕ} (L : List (PauliString n)) {kh : ℕ} (hL : IsLayer kh L) (p : PauliIndex n) : (antiLayer L p).card ≤ wt p

Disjoint supports bound the number of anticommuting generators by the Pauli weight. This is the combinatorial statement |𝒜(p)| ≤ |p| in apd:thm:layer_inflow: every anticommuting generator meets the support of p, and distinct generators of a layer meet it in disjoint sets of sites.

theorem Lean4LPD.PauliString.card_antiLayer_powersetCard_le {n : ℕ} (L : List (PauliString n)) {kh : ℕ} (hL : IsLayer kh L) (p : PauliIndex n) (j : ℕ) : (Finset.powersetCard j (antiLayer L p)).card ≤ (wt p).choose j

The number of j-element subsets of 𝒜(p) is at most C(|p|, j). This is the subset-counting part of the row and column estimates in apd:thm:layer_inflow. The matrix entries themselves are bounded in row_sum_norm_layerJumpMatrix_le and col_sum_norm_layerJumpMatrix_le, through layerAntiCount.

theorem Lean4LPD.PauliString.sympForm_herm_partner_of_commute {n : ℕ} (G H : PauliString n) (hGH : G.sympForm H = 0) (p : PauliIndex n) : G.sympForm (herm (H.partner p)) = G.sympForm (herm p)

Commuting with a generator makes its partner translation preserve the symplectic test against another generator. Supporting lemma for the fixed 𝒜(p) in apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.antiLayer_partner {n : ℕ} (L : List (PauliString n)) (H : PauliString n) (hH : ∀ G ∈ L, G.sympForm H = 0) (p : PauliIndex n) : antiLayer L (H.partner p) = antiLayer L p

Taking any generator in a commuting layer leaves the entire anticommutation set unchanged. Supporting lemma for apd:thm:layer_inflow. Disjointness is a sufficient condition, but pairwise commutation is exactly what this identity needs.

noncomputable def Lean4LPD.PauliString.layerSigma {n : ℕ} : List (PauliString n × ℝ) → ℝ

The largest absolute sine max_l |sin θ_l| of a layer, with value 0 for the empty layer. Stating apd:thm:layer_inflow with this parameter makes the bound valid for arbitrary angles: monotonicity of sine on an interval of angles is never needed.

Equations

• Lean4LPD.PauliString.layerSigma [] = 0
• Lean4LPD.PauliString.layerSigma (g :: L) = max |Real.sin g.2| (Lean4LPD.PauliString.layerSigma L)

theorem Lean4LPD.PauliString.layerSigma_nonneg {n : ℕ} (L : List (PauliString n × ℝ)) : 0 ≤ layerSigma L

The layer's largest absolute sine is nonnegative; supporting lemma for apd:thm:layer_inflow with the parameter σ = layerSigma L.

theorem Lean4LPD.PauliString.abs_sin_le_layerSigma {n : ℕ} (L : List (PauliString n × ℝ)) (g : PauliString n × ℝ) (hg : g ∈ L) : |Real.sin g.2| ≤ layerSigma L

Every individual sine magnitude is bounded by the layer parameter. Supporting lemma for apd:thm:layer_inflow.

noncomputable def Lean4LPD.PauliString.layerJumpMatrix {n : ℕ} (L : List (PauliString n × ℝ)) (j : ℕ) : Matrix (PauliIndex n) (PauliIndex n) ℂ

The matrix of the exactly-j component layerJump L j: its column q is the image of the basis vector at q. Supporting definition for A^{(j)} in apd:thm:layer_inflow; the restriction to high-weight rows and low-weight columns is layerInflowMatrix.

Equations

• Lean4LPD.PauliString.layerJumpMatrix L j p q = (Lean4LPD.PauliString.layerJump L j (WithLp.toLp 2 (Pi.single q 1))).ofLp p

theorem Lean4LPD.PauliString.layerJump_apply_eq_sum_matrix {n : ℕ} (L : List (PauliString n × ℝ)) (j : ℕ) (y : EuclideanSpace ℂ (PauliIndex n)) (p : PauliIndex n) : (layerJump L j y).ofLp p = ∑ q : PauliIndex n, layerJumpMatrix L j p q * y.ofLp q

layerJumpMatrix L j acts on an arbitrary coefficient vector as layerJump L j does, not only on basis vectors. Supporting lemma for apd:thm:layer_inflow.

def Lean4LPD.PauliString.layerAntiCount {n : ℕ} (L : List (PauliString n)) (p : PauliIndex n) : ℕ

The number of anticommuting rotations, retaining list multiplicity. In a disjoint layer this equals |𝒜(p)|; in a merely commuting layer it may be system-size dependent. Supporting definition for apd:thm:layer_inflow.

Equations

• Lean4LPD.PauliString.layerAntiCount L p = List.countP (fun (G : Lean4LPD.PauliString n) => decide (G.sympForm (Lean4LPD.PauliString.herm p) = 1)) L

theorem Lean4LPD.PauliString.layerAntiCount_partner {n : ℕ} (L : List (PauliString n)) (G : PauliString n) (hG : ∀ H ∈ L, H.sympForm G = 0) (p : PauliIndex n) : layerAntiCount L (G.partner p) = layerAntiCount L p

Partner translation in a commuting layer preserves its anticommuting-rotation count. Supporting lemma for apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.layerJumpMatrix_eq_zero_of_sympForm_ne {n : ℕ} (L : List (PauliString n × ℝ)) (G : PauliString n) (hG : ∀ g ∈ L, G.sympForm g.1 = 0) (j : ℕ) (p q : PauliIndex n) (hpq : G.sympForm (herm p) ≠ G.sympForm (herm q)) : layerJumpMatrix L j p q = 0

Branches through generators that commute with G preserve the commutation class with G: the entry (p, q) of layerJumpMatrix L j vanishes unless p and q have the same symplectic form with G. Supporting lemma for the column estimate of apd:thm:layer_inflow. This is finer than support containment: it shows that an input Pauli commuting with G never takes the sine branch of G.

theorem Lean4LPD.PauliString.norm_stayAct_apply_le {n : ℕ} (G : PauliString n) (θ : ℝ) (y : EuclideanSpace ℂ (PauliIndex n)) (p : PauliIndex n) : ‖(G.stayAct θ y).ofLp p‖ ≤ ‖y.ofLp p‖

The unchanged branch is a contraction in each coefficient magnitude. Supporting lemma for apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.norm_jumpAct_apply_le {n : ℕ} (G : PauliString n) (θ : ℝ) (y : EuclideanSpace ℂ (PauliIndex n)) (p : PauliIndex n) : ‖(G.jumpAct θ y).ofLp p‖ ≤ |Real.sin θ| * ‖y.ofLp (G.partner p)‖

The sine-branch coefficient is bounded by the absolute sine times its partner coefficient. Supporting lemma for apd:thm:layer_inflow. No Hermitian hypothesis is needed for this magnitude statement: partnerSign is always a fourth root of unity.

theorem Lean4LPD.PauliString.sum_norm_stayAct_le {n : ℕ} (G : PauliString n) (θ : ℝ) (y : EuclideanSpace ℂ (PauliIndex n)) : ∑ p : PauliIndex n, ‖(G.stayAct θ y).ofLp p‖ ≤ ∑ p : PauliIndex n, ‖y.ofLp p‖

The unchanged branch contracts the coefficient ℓ¹ norm. Supporting lemma for the column estimate of apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.sum_norm_jumpAct_le {n : ℕ} (G : PauliString n) (θ : ℝ) (y : EuclideanSpace ℂ (PauliIndex n)) : ∑ p : PauliIndex n, ‖(G.jumpAct θ y).ofLp p‖ ≤ |Real.sin θ| * ∑ p : PauliIndex n, ‖y.ofLp p‖

The sine branch contracts the coefficient ℓ¹ norm by its absolute sine. Supporting lemma for the column estimate of apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.layerAntiCount_eq_card_antiLayer {n : ℕ} (L : List (PauliString n)) {kh : ℕ} (hL : IsLayer kh L) (p : PauliIndex n) : layerAntiCount L p = (antiLayer L p).card

In a disjoint layer the list count has no anticommuting duplicates, so it is exactly the finite-set cardinality |𝒜(p)|. Supporting lemma for apd:thm:layer_inflow. Repeated scalar generators are harmless because they never anticommute.

theorem Lean4LPD.PauliString.layerAntiCount_le_weight {n : ℕ} (L : List (PauliString n)) {kh : ℕ} (hL : IsLayer kh L) (p : PauliIndex n) : layerAntiCount L p ≤ wt p

The anticommuting-rotation list count is bounded by Pauli weight for a disjoint layer. Supporting lemma for apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.row_sum_norm_layerJumpMatrix_le {n : ℕ} (L : List (PauliString n × ℝ)) (hcomm : ∀ g ∈ L, ∀ h ∈ L, g.1.sympForm h.1 = 0) {σ : ℝ} (hσ : 0 ≤ σ) (hsin : ∀ g ∈ L, |Real.sin g.2| ≤ σ) (j : ℕ) (p : PauliIndex n) : ∑ q : PauliIndex n, ‖layerJumpMatrix L j p q‖ ≤ ↑((layerAntiCount (List.map Prod.fst L) p).choose j) * σ ^ j

Absolute row sums of the exactly-j matrix. Row p of layerJumpMatrix L j has absolute sum at most C(c, j) σ^j, where c is the number of rotations of the layer that anticommute with p. Supporting theorem for the Schur step in apd:thm:layer_inflow. Pairwise commutation suffices for this estimate; disjoint supports are used afterwards, to bound layerAntiCount by the Pauli weight of p.

theorem Lean4LPD.PauliString.jumpAct_layerJump_single_eq_zero {n : ℕ} (L : List (PauliString n × ℝ)) (G : PauliString n) (θ : ℝ) (hG : ∀ g ∈ L, G.sympForm g.1 = 0) (j : ℕ) (q : PauliIndex n) (hq : G.sympForm (herm q) = 0) : G.jumpAct θ (layerJump L j (WithLp.toLp 2 (Pi.single q 1))) = 0

If the input Pauli q commutes with G, and G commutes with every generator of L, then the sine branch of G annihilates layerJump L j of the basis vector at q. Supporting lemma for the column estimate of apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.col_sum_norm_layerJumpMatrix_le {n : ℕ} (L : List (PauliString n × ℝ)) (hcomm : ∀ g ∈ L, ∀ h ∈ L, g.1.sympForm h.1 = 0) {σ : ℝ} (hσ : 0 ≤ σ) (hsin : ∀ g ∈ L, |Real.sin g.2| ≤ σ) (j : ℕ) (q : PauliIndex n) : ∑ p : PauliIndex n, ‖layerJumpMatrix L j p q‖ ≤ ↑((layerAntiCount (List.map Prod.fst L) q).choose j) * σ ^ j

Absolute column sums of the exactly-j matrix. Column q of layerJumpMatrix L j has absolute sum at most C(c, j) σ^j, where c is the number of rotations of the layer that anticommute with q. Supporting theorem for the Schur step in apd:thm:layer_inflow. The proof uses preservation of the commutation class (jumpAct_layerJump_single_eq_zero) and Pascal's rule; it does not assume that distinct choices of branches give distinct nonzero entries.

theorem Lean4LPD.PauliString.layer_sympForm_eq_zero {n : ℕ} (L : List (PauliString n × ℝ)) {kh : ℕ} (hL : IsLayer kh (List.map Prod.fst L)) (g : PauliString n × ℝ) : g ∈ L → ∀ h ∈ L, g.1.sympForm h.1 = 0

Disjoint supports imply the pairwise commutation used by the exactly-j row and column estimates. Supporting lemma for apd:thm:layer_inflow.

noncomputable def Lean4LPD.PauliString.layerInflowMatrix {n : ℕ} (L : List (PauliString n × ℝ)) (w j : ℕ) : Matrix (PauliIndex n) (PauliIndex n) ℂ

The exactly-j matrix restricted to rows of weight > w and columns of weight ≤ w. This is A^{(j)} in apd:thm:layer_inflow, represented on the full coefficient space by filling the other blocks with zeros.

Equations

• Lean4LPD.PauliString.layerInflowMatrix L w j p q = if w < Lean4LPD.PauliString.wt p ∧ Lean4LPD.PauliString.wt q ≤ w then Lean4LPD.PauliString.layerJumpMatrix L j p q else 0

theorem Lean4LPD.PauliString.row_sum_norm_layerInflowMatrix_le {n : ℕ} (L : List (PauliString n × ℝ)) {kh : ℕ} (hL : IsLayer kh (List.map Prod.fst L)) {σ : ℝ} (hσ : 0 ≤ σ) (hsin : ∀ g ∈ L, |Real.sin g.2| ≤ σ) (w j : ℕ) (p : PauliIndex n) : ∑ q : PauliIndex n, ‖layerInflowMatrix L w j p q‖ ≤ ↑((w + j * (kh - 1)).choose j) * σ ^ j

Row bound for the high-from-low exactly-j block. Formalizes the row estimate of apd:thm:layer_inflow: a nonzero row has weight at most w + j (k_h - 1) by layerJump_single_eq_zero_of_weight_lt, and in a disjoint-support layer at most that many generators anticommute with it.

theorem Lean4LPD.PauliString.col_sum_norm_layerInflowMatrix_le {n : ℕ} (L : List (PauliString n × ℝ)) {kh : ℕ} (hL : IsLayer kh (List.map Prod.fst L)) {σ : ℝ} (hσ : 0 ≤ σ) (hsin : ∀ g ∈ L, |Real.sin g.2| ≤ σ) (w j : ℕ) (q : PauliIndex n) : ∑ p : PauliIndex n, ‖layerInflowMatrix L w j p q‖ ≤ ↑(w.choose j) * σ ^ j

Column bound for the high-from-low exactly-j block. Formalizes the column estimate of apd:thm:layer_inflow: a nonzero column has weight at most w. The angles are unrestricted and enter only through the bound σ on their absolute sines.

theorem Lean4LPD.PauliString.norm_layerInflowMatrix_le {n : ℕ} (L : List (PauliString n × ℝ)) {kh : ℕ} (hL : IsLayer kh (List.map Prod.fst L)) {σ : ℝ} (hσ : 0 ≤ σ) (hsin : ∀ g ∈ L, |Real.sin g.2| ≤ σ) (w j : ℕ) : ‖layerInflowMatrix L w j‖ ≤ ↑((w + j * (kh - 1)).choose j) * σ ^ j

Layer inflow, binomial form. Formalizes the first inequality of apd:eq:layer_inflow in apd:thm:layer_inflow, for any σ dominating every absolute sine and an arbitrary threshold w. The Schur test combines the row bound with the (smaller) column bound. The matrix is built from the rotations themselves, so no flow inequality is assumed. At w = w_m, the upper weight is w_m + j (k_h - 1) = w_{m+j} for m ≥ 1.

theorem Lean4LPD.PauliString.norm_layerInflowMatrix_le_layerSigma {n : ℕ} (L : List (PauliString n × ℝ)) {kh : ℕ} (hL : IsLayer kh (List.map Prod.fst L)) (w j : ℕ) : ‖layerInflowMatrix L w j‖ ≤ ↑((w + j * (kh - 1)).choose j) * layerSigma L ^ j

The layer-inflow bound with no hypothesis on the angles: apd:eq:layer_inflow with σ = max_l |sin θ_l|. Neither positivity of the sines nor monotonicity of sine on an interval of angles is required, which is more general than the paper's statement.

theorem Lean4LPD.PauliString.norm_layerInflowMatrix_le_factorial {n : ℕ} (L : List (PauliString n × ℝ)) {kh : ℕ} (hL : IsLayer kh (List.map Prod.fst L)) {σ : ℝ} (hσ : 0 ≤ σ) (hsin : ∀ g ∈ L, |Real.sin g.2| ≤ σ) (w j : ℕ) : ‖layerInflowMatrix L w j‖ ≤ (↑(w + j * (kh - 1)) * σ) ^ j / ↑j.factorial

Layer inflow, factorial form. Formalizes the second inequality of apd:eq:layer_inflow, C(W, j) σ^j ≤ (W σ)^j / j! with W = w + j (k_h - 1), for the absolute-sine parameter σ and an arbitrary natural weight threshold w.

theorem Lean4LPD.PauliString.layerInflowMatrix_mulVec {n : ℕ} (L : List (PauliString n × ℝ)) (w j : ℕ) (y : EuclideanSpace ℂ (PauliIndex n)) : WithLp.toLp 2 ((layerInflowMatrix L w j).mulVec y.ofLp) = restr (highSet n w) (layerJump L j (restr (highSet n w)ᶜ y))

layerInflowMatrix L w j acts as layerJump L j restricted to low-weight inputs and high-weight outputs. This connects the Schur bound to the Pauli coefficients of the conjugated operator in apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.layerInflowMatrix_zero {n : ℕ} (L : List (PauliString n × ℝ)) (w : ℕ) : layerInflowMatrix L w 0 = 0

The zero-sine branch is diagonal, so its high-from-low block vanishes. Supporting lemma for A_RB = ∑_{j≥1} A^{(j)} in apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.layerAct_add {n : ℕ} (L : List (PauliString n × ℝ)) (y z : EuclideanSpace ℂ (PauliIndex n)) : layerAct L (y + z) = layerAct L y + layerAct L z

Additivity of the layer action on coefficient vectors. Supporting lemma for the high/low split in apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.restr_sum {n : ℕ} {ι : Type u_1} (s : Finset ι) (R : Finset (PauliIndex n)) (f : ι → EuclideanSpace ℂ (PauliIndex n)) : restr R (∑ i ∈ s, f i) = ∑ i ∈ s, restr R (f i)

Finite-sum compatibility of coefficient projection. Supporting lemma for A_RB = ∑_{j≥1} A^{(j)} in apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.restr_layerAct_low_eq_sum_inflow {n : ℕ} (L : List (PauliString n × ℝ)) (w : ℕ) (y : EuclideanSpace ℂ (PauliIndex n)) : restr (highSet n w) (layerAct L (restr (highSet n w)ᶜ y)) = ∑ j ∈ Finset.range (L.length + 1), (clm (layerInflowMatrix L w j)) y

The high-from-low block of a layer is the sum of its exactly-j blocks. This is the action form of A_RB = ∑_{j≥1} A^{(j)} in apd:thm:layer_inflow. The finite sum runs over 0 ≤ j ≤ L.length; its j = 0 term vanishes by layerInflowMatrix_zero.

theorem Lean4LPD.PauliString.norm_restr_layerAct_le_sum_inflow {n : ℕ} (L : List (PauliString n × ℝ)) (hL : ∀ g ∈ L, IsSelfAdjoint g.1) (w : ℕ) (y : EuclideanSpace ℂ (PauliIndex n)) : ‖restr (highSet n w) (layerAct L y)‖ ≤ ‖restr (highSet n w) y‖ + ∑ j ∈ Finset.range (L.length + 1), ‖(clm (layerInflowMatrix L w j)) y‖

High-weight norm after a layer: the previous high-weight norm plus the inflows. The triangle inequality applied to the block decomposition of apd:thm:layer_inflow: the high-to-high block is a contraction because the layer is an isometry (norm_layerAct), and the high-from-low block is the sum of the A^{(j)}. Both facts are proved above from the rotations, so no flow inequality is assumed.

theorem Lean4LPD.PauliString.layerInflowMatrix_clm_restr {n : ℕ} (L : List (PauliString n × ℝ)) {kh w w' j : ℕ} (hk : ∀ g ∈ L, g.1.weight ≤ kh) (hw : w' + j * (kh - 1) ≤ w) (y : EuclideanSpace ℂ (PauliIndex n)) : (clm (layerInflowMatrix L w j)) y = (clm (layerInflowMatrix L w j)) (restr (highSet n w') y)

A j-jump inflow into weights above w only uses the input's coefficients of weight above w', for any w' with w' + j (k_h - 1) ≤ w. This localizes the inflow on the lower rung, as needed by apd:rmk:multijump; it follows from the coefficient support bound in apd:thm:layer_inflow.

theorem Lean4LPD.PauliString.norm_layerInflowMatrix_clm_le {n : ℕ} (L : List (PauliString n × ℝ)) {kh : ℕ} (hL : IsLayer kh (List.map Prod.fst L)) {σ : ℝ} (hσ : 0 ≤ σ) (hsin : ∀ g ∈ L, |Real.sin g.2| ≤ σ) (w j : ℕ) (y : EuclideanSpace ℂ (PauliIndex n)) : ‖(clm (layerInflowMatrix L w j)) y‖ ≤ (↑(w + j * (kh - 1)) * σ) ^ j / ↑j.factorial * ‖y‖

The j-jump inflow of a coefficient vector is bounded by the factorial inflow factor times the norm of the vector. Supporting theorem for apd:thm:layer_inflow and the multi-jump recursion in apd:rmk:multijump.

theorem Lean4LPD.PauliString.norm_layerInflowMatrix_clm_le_restr {n : ℕ} (L : List (PauliString n × ℝ)) {kh w w' j : ℕ} (hL : IsLayer kh (List.map Prod.fst L)) {σ : ℝ} (hσ : 0 ≤ σ) (hsin : ∀ g ∈ L, |Real.sin g.2| ≤ σ) (hw : w' + j * (kh - 1) ≤ w) (y : EuclideanSpace ℂ (PauliIndex n)) : ‖(clm (layerInflowMatrix L w j)) y‖ ≤ (↑(w + j * (kh - 1)) * σ) ^ j / ↑j.factorial * ‖restr (highSet n w') y‖

The j-jump inflow bounded by the input's norm above the lower threshold w', where w' + j (k_h - 1) ≤ w. Supporting theorem for apd:rmk:multijump; the coefficient is the one proved in apd:thm:layer_inflow.