Shared finite Schur test

The finite rectangular Schur test over an RCLike field, together with its rowwise, sum-of-squares, and continuous-linear-map formulations. Empty index types are allowed.

Moved from LeanPool.LowWeightPauliDynamics.Schur and its matrix-map abbreviation from LeanPool.LowWeightPauliDynamics.BlockNorm, preserving Jue Xu's proofs and public names. This lightweight module depends only on Mathlib and is shared by the Pauli-dynamics and block/spectral-sensitivity developments.

@[reducible, inline]

noncomputable abbrev Lean4LPD.clm {𝕜 : Type u_1} [RCLike 𝕜] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m

The continuous linear map on EuclideanSpace attached to a (possibly rectangular) matrix. This is the map whose operator norm is ‖A‖ for the scoped ℓ² operator norm, by Matrix.l2_opNorm_def; for square matrices it agrees with Matrix.toEuclideanCLM.

Equations

• Lean4LPD.clm A = (Matrix.toEuclideanLin.trans LinearMap.toContinuousLinearMap) A

theorem Lean4LPD.schur_row_sq_le {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {κ : Type u_3} [Fintype κ] (A : Matrix ι κ 𝕜) (y : κ → 𝕜) (i : ι) (R : ℝ) (hrow : ∑ j : κ, ‖A i j‖ ≤ R) : ‖A.mulVec y i‖ ^ 2 ≤ R * ∑ j : κ, ‖A i j‖ * ‖y j‖ ^ 2

Weighted Cauchy–Schwarz for one row: if row i of A has absolute sum at most R, then ‖(A *ᵥ y) i‖ ^ 2 ≤ R * ∑ j, ‖A i j‖ * ‖y j‖ ^ 2. This is the row step of the Schur test used in apd:thm:layer_inflow. Zero entries and empty sums need no separate case.

theorem Lean4LPD.schur_mulVec_sq_le {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] (A : Matrix ι κ 𝕜) (y : κ → 𝕜) {R C : ℝ} (hR : 0 ≤ R) (hrow : ∀ (i : ι), ∑ j : κ, ‖A i j‖ ≤ R) (hcol : ∀ (j : κ), ∑ i : ι, ‖A i j‖ ≤ C) : ∑ i : ι, ‖A.mulVec y i‖ ^ 2 ≤ R * C * ∑ j : κ, ‖y j‖ ^ 2

Squared form of the finite Schur test used in apd:thm:layer_inflow: if every row of A has absolute sum at most R and every column at most C, then ∑ i, ‖(A *ᵥ y) i‖ ^ 2 ≤ R * C * ∑ j, ‖y j‖ ^ 2.

theorem Lean4LPD.schur_clm_le {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq κ] (A : Matrix ι κ 𝕜) (y : EuclideanSpace 𝕜 κ) {R C : ℝ} (hR : 0 ≤ R) (hC : 0 ≤ C) (hrow : ∀ (i : ι), ∑ j : κ, ‖A i j‖ ≤ R) (hcol : ∀ (j : κ), ∑ i : ι, ‖A i j‖ ≤ C) : ‖(clm A) y‖ ≤ √(R * C) * ‖y‖

The Schur test as a bound on the action of clm A, the continuous linear map of Euclidean spaces attached to A in BlockNorm: ‖clm A y‖ ≤ √(R * C) * ‖y‖ (apd:thm:layer_inflow).

theorem Lean4LPD.schur_mulVec_le {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] (A : Matrix ι κ 𝕜) (y : EuclideanSpace 𝕜 κ) {R C : ℝ} (hR : 0 ≤ R) (hC : 0 ≤ C) (hrow : ∀ (i : ι), ∑ j : κ, ‖A i j‖ ≤ R) (hcol : ∀ (j : κ), ∑ i : ι, ‖A i j‖ ≤ C) : ‖WithLp.toLp 2 (A.mulVec y.ofLp)‖ ≤ √(R * C) * ‖y‖

The same bound for Matrix.mulVec, without the bundled map clm A. The norm is the Euclidean norm that Pauli coefficient vectors carry (apd:thm:layer_inflow).

theorem Lean4LPD.l2_opNorm_le_schur {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq κ] (A : Matrix ι κ 𝕜) {R C : ℝ} (hR : 0 ≤ R) (hC : 0 ≤ C) (hrow : ∀ (i : ι), ∑ j : κ, ‖A i j‖ ≤ R) (hcol : ∀ (j : κ), ∑ i : ι, ‖A i j‖ ≤ C) : ‖A‖ ≤ √(R * C)

The finite Schur test, in the form used by apd:thm:layer_inflow: row sums at most R and column sums at most C give ‖A‖ ≤ √(R * C). Here ‖A‖ is the scoped ℓ² operator norm (Matrix.Norms.L2Operator), not an entrywise matrix norm.

theorem Lean4LPD.l2_opNorm_le_of_row_col_bound {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq κ] (A : Matrix ι κ 𝕜) {B : ℝ} (hB : 0 ≤ B) (hrow : ∀ (i : ι), ∑ j : κ, ‖A i j‖ ≤ B) (hcol : ∀ (j : κ), ∑ i : ι, ‖A i j‖ ≤ B) : ‖A‖ ≤ B

If B bounds every row sum and every column sum, then ‖A‖ ≤ B: the case R = C = B of l2_opNorm_le_schur. This is the form Pauli/LayerFlow applies to the layer inflow matrices (apd:thm:layer_inflow).