The ℓ² operator norm of a block of a matrix

A block of a matrix has ℓ² operator norm at most that of the matrix; in particular every block of a unitary matrix, or of a real orthogonal matrix, has ℓ² operator norm at most one. The proof of apd:thm:local_flow_k_local uses this for the orthogonal matrix A by which a Pauli rotation acts on the vector of Pauli coefficients: the block A_RR of A on the high-weight coordinates R satisfies ‖A_RR‖ ≤ ‖A‖ = 1. That is the first of the two estimates the damped flow recursion rests on.

The statement is proved in more generality than this application needs: for any pair of injective index maps, over any RCLike field, and with no nonemptiness hypothesis. Nothing here is specific to Pauli strings. Pauli/Flow does not go through this file: it never builds the matrix A, and proves the same estimate directly on coefficient vectors. This file is the matrix form of the statement, and its clm is how Schur and the layer inflow bounds speak about the ℓ² operator norm of a rectangular matrix.

Main definitions

• restrictCLM: restriction of coordinates along an index map, as a continuous linear map of Euclidean spaces.
• clm: the continuous linear map of Euclidean spaces attached to a rectangular matrix; its operator norm is the ℓ² operator norm of the matrix.

Main results

• l2_opNorm_submatrix_le: ‖A.submatrix f g‖ ≤ ‖A‖ for injective f and g.
• l2_opNorm_toBlock_le: the same for Matrix.toBlock.
• l2_opNorm_submatrix_le_one_of_mem_unitary, l2_opNorm_toBlock_le_one_of_mem_unitary: a block of a unitary matrix has ℓ² operator norm at most one.
• l2_opNorm_submatrix_le_one_of_mem_orthogonalGroup, l2_opNorm_toBlock_le_one_of_mem_orthogonalGroup: the real orthogonal case.

Method

Matrix.l2_opNorm_def says that the rectangular ℓ² operator norm is the operator norm of a continuous linear map, by rfl. Selecting rows then factors definitionally,

clm (A.submatrix f id) = restrictCLM 𝕜 f ∘L clm A — also rfl,

so ContinuousLinearMap.opNorm_comp_le does the work once coordinate restriction is shown to be a contraction. Columns come from conjugate-transposing rather than from a second map. No singular values and no spectral theory are needed.

Injectivity is needed

Both index maps must be injective. Repeating the single row of the 1 × 1 identity gives a 2 × 1 block of norm √2 > 1 = ‖1‖; that witness is example-checked at the end of the file.

The coordinate-restriction continuous linear map

noncomputable def Lean4LPD.restrictCLM (𝕜 : Type u_2) [RCLike 𝕜] {p : Type u_3} {m : Type u_4} (f : p → m) : EuclideanSpace 𝕜 m →L[𝕜] EuclideanSpace 𝕜 p

Restriction of coordinates along f : p → m, as a continuous linear map of Euclidean spaces: x ↦ x ∘ f. Mathlib's EuclideanSpace.restrict₂ covers only the inclusion of one Finset in another and comes with no norm lemma.

Equations

• Lean4LPD.restrictCLM 𝕜 f = { toFun := fun (x : EuclideanSpace 𝕜 m) => WithLp.toLp 2 fun (i : p) => x.ofLp (f i), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem Lean4LPD.restrictCLM_apply {𝕜 : Type u_1} [RCLike 𝕜] {p : Type u_2} {m : Type u_3} (f : p → m) (x : EuclideanSpace 𝕜 m) (i : p) : ((restrictCLM 𝕜 f) x).ofLp i = x.ofLp (f i)

theorem Lean4LPD.norm_restrictCLM_apply_le {𝕜 : Type u_1} [RCLike 𝕜] {m : Type u_2} {p : Type u_3} [Fintype m] [Fintype p] {f : p → m} (hf : Function.Injective f) (x : EuclideanSpace 𝕜 m) : ‖(restrictCLM 𝕜 f) x‖ ≤ ‖x‖

Dropping coordinates (along an injective map) does not increase the ℓ² norm.

theorem Lean4LPD.norm_restrictCLM_le_one {𝕜 : Type u_1} [RCLike 𝕜] {m : Type u_2} {p : Type u_3} [Fintype m] [Fintype p] {f : p → m} (hf : Function.Injective f) : ‖restrictCLM 𝕜 f‖ ≤ 1

Coordinate restriction along an injective map is a contraction.

Selecting rows, then columns

theorem Lean4LPD.clm_submatrix_id {𝕜 : Type u_1} [RCLike 𝕜] {m : Type u_2} {n : Type u_3} {p : Type u_4} [Fintype m] [Fintype n] [Fintype p] [DecidableEq n] (A : Matrix m n 𝕜) (f : p → m) : clm (A.submatrix f id) = restrictCLM 𝕜 f ∘SL clm A

Selecting a subfamily of rows factors, definitionally, through coordinate restriction: clm (A.submatrix f id) = restrictCLM 𝕜 f ∘L clm A.

theorem Lean4LPD.l2_opNorm_submatrix_id_le {𝕜 : Type u_1} [RCLike 𝕜] {m : Type u_2} {n : Type u_3} {p : Type u_4} [Fintype m] [Fintype n] [Fintype p] [DecidableEq n] (A : Matrix m n 𝕜) {f : p → m} (hf : Function.Injective f) : ‖A.submatrix f id‖ ≤ ‖A‖

Row selection does not increase the ℓ² operator norm.

theorem Lean4LPD.l2_opNorm_submatrix_le {𝕜 : Type u_1} [RCLike 𝕜] {m : Type u_2} {n : Type u_3} {p : Type u_4} {q : Type u_5} [Fintype m] [Fintype n] [Fintype p] [Fintype q] [DecidableEq n] [DecidableEq q] (A : Matrix m n 𝕜) {f : p → m} {g : q → n} (hf : Function.Injective f) (hg : Function.Injective g) : ‖A.submatrix f g‖ ≤ ‖A‖

A block of a matrix has ℓ² operator norm at most that of the matrix.

A.submatrix f g selects the rows indexed by f and the columns indexed by g. Both index maps are required to be injective, and that hypothesis cannot be dropped: repeating the single row of the 1 × 1 identity gives a matrix of norm √2 (see the last example of this file).

The proof selects rows with l2_opNorm_submatrix_id_le, conjugate-transposes, and selects rows again.

theorem Lean4LPD.l2_opNorm_toBlock_le {𝕜 : Type u_1} [RCLike 𝕜] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) (P : m → Prop) (Q : n → Prop) [DecidablePred P] [DecidablePred Q] : ‖A.toBlock P Q‖ ≤ ‖A‖

Matrix.toBlock form of l2_opNorm_submatrix_le.

Unitary and orthogonal matrices

theorem Lean4LPD.l2_opNorm_le_one_of_mem_unitary {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] {U : Matrix n n 𝕜} (hU : U ∈ unitary (Matrix n n 𝕜)) : ‖U‖ ≤ 1

‖U‖ ≤ 1 for a unitary U, with no nonemptiness hypothesis. CStarRing.norm_of_mem_unitary would need [Nontrivial (Matrix n n 𝕜)], hence [Nonempty n], but CStarRing.norm_mul_mem_unitary needs none, and ‖(1 : Matrix n n 𝕜)‖ ≤ 1 holds even when n is empty (the matrix ring is then trivial, so 1 = 0 and ‖1‖ = 0).

theorem Lean4LPD.l2_opNorm_submatrix_le_one_of_mem_unitary {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_3} {p : Type u_4} {q : Type u_5} [Fintype n] [Fintype p] [Fintype q] [DecidableEq n] [DecidableEq q] {U : Matrix n n 𝕜} (hU : U ∈ unitary (Matrix n n 𝕜)) {f : p → n} {g : q → n} (hf : Function.Injective f) (hg : Function.Injective g) : ‖U.submatrix f g‖ ≤ 1

A block of a unitary matrix has ℓ² operator norm at most 1.

f and g are injective index maps, e.g. Subtype.val out of the two index subtypes cutting the block out. No nonemptiness hypothesis on any of n, p, q.

theorem Lean4LPD.l2_opNorm_submatrix_le_one_of_mem_unitaryGroup {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_3} {p : Type u_4} {q : Type u_5} [Fintype n] [Fintype p] [Fintype q] [DecidableEq n] [DecidableEq q] {U : Matrix n n 𝕜} (hU : U ∈ Matrix.unitaryGroup n 𝕜) {f : p → n} {g : q → n} (hf : Function.Injective f) (hg : Function.Injective g) : ‖U.submatrix f g‖ ≤ 1

Matrix.unitaryGroup spelling.

theorem Lean4LPD.l2_opNorm_toBlock_le_one_of_mem_unitary {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] {U : Matrix n n 𝕜} (hU : U ∈ unitary (Matrix n n 𝕜)) (P Q : n → Prop) [DecidablePred P] [DecidablePred Q] : ‖U.toBlock P Q‖ ≤ 1

Matrix.toBlock form: the (P, Q) block of a unitary has ℓ² operator norm at most 1.

theorem Lean4LPD.l2_opNorm_submatrix_le_one_of_mem_orthogonalGroup {n : Type u_3} {p : Type u_4} {q : Type u_5} [Fintype n] [Fintype p] [Fintype q] [DecidableEq n] [DecidableEq q] {O : Matrix n n ℝ} (hO : O ∈ Matrix.orthogonalGroup n ℝ) {f : p → n} {g : q → n} (hf : Function.Injective f) (hg : Function.Injective g) : ‖O.submatrix f g‖ ≤ 1

Real orthogonal case, the 𝕜 = ℝ specialization: a block of an orthogonal matrix has ℓ² operator norm at most 1. Matrix.orthogonalGroup n ℝ is by definition unitary (Matrix n n ℝ) with the trivial star, so this is literally the unitary statement at 𝕜 = ℝ.

theorem Lean4LPD.l2_opNorm_toBlock_le_one_of_mem_orthogonalGroup {n : Type u_3} [Fintype n] [DecidableEq n] {O : Matrix n n ℝ} (hO : O ∈ Matrix.orthogonalGroup n ℝ) (P Q : n → Prop) [DecidablePred P] [DecidablePred Q] : ‖O.toBlock P Q‖ ≤ 1

Matrix.toBlock form of the orthogonal case.

Sanity checks