The Schur test for the L2 operator norm

General real-matrix lemmas about the L2 operator norm, used in Section 11.3 of bs_lambda.txt, where the oriented overlap matrix R is bounded through ‖R‖₂ ≤ sqrt (‖R‖₁ ‖R‖∞), i.e. by the geometric mean of the maximum column sum and the maximum row sum.

The nonnegative real specialization below reuses Lean4LPD.l2_opNorm_le_schur, the pool's finite rectangular Schur test over any RCLike field. The shared module depends only on Mathlib. The other lemmas expose convenient real-matrix formulations for the spectral-sensitivity development.

Adapted for Lean Pool from Timeroot/BS_Lam at commit 7bd39a8d41ee7910d3296d0477ad18f8fff9d870; ported to Lean Pool with proof and dependency cleanup.

theorem Matrix.l2_opNorm_transpose {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] [DecidableEq n] [DecidableEq m] (A : Matrix m n ℝ) : ‖A.transpose‖ = ‖A‖

Over ℝ the transpose coincides with the conjugate transpose, so it preserves the L2 operator norm.

theorem Matrix.l2_opNorm_le_of_norm_mulVec_le {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] [DecidableEq n] {C : ℝ} (A : Matrix m n ℝ) (hC : 0 ≤ C) (h : ∀ (v : EuclideanSpace ℝ n), ‖(EuclideanSpace.equiv m ℝ).symm (A.mulVec v.ofLp)‖ ≤ C * ‖v‖) : ‖A‖ ≤ C

Converse of Matrix.l2_opNorm_mulVec: if every Euclidean vector v satisfies ‖A *ᵥ v‖ ≤ C * ‖v‖, then the L2 operator norm of A is at most C. This is the entry point for the Schur test of Section 11.3 of bs_lambda.txt.

theorem Matrix.l2_opNorm_le_of_sum_sq_mulVec_le {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] [DecidableEq n] {C : ℝ} (A : Matrix m n ℝ) (hC : 0 ≤ C) (h : ∀ (v : n → ℝ), ∑ i : m, A.mulVec v i ^ 2 ≤ C ^ 2 * ∑ j : n, v j ^ 2) : ‖A‖ ≤ C

Sum-level form of Matrix.l2_opNorm_le_of_norm_mulVec_le: it suffices to bound ∑ i, (A *ᵥ v) i ^ 2 by C ^ 2 * ∑ j, v j ^ 2 for every plain vector v. Used for the Schur test in Section 11.3 of bs_lambda.txt.

theorem Matrix.sum_sq_mulVec_le {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n ℝ) (v : n → ℝ) : ∑ i : m, A.mulVec v i ^ 2 ≤ ‖A‖ ^ 2 * ∑ j : n, v j ^ 2

Sum form of Matrix.l2_opNorm_mulVec: the defining operator bound, with both norms squared and written out as sums.

theorem Matrix.l2_opNorm_le_sqrt_of_row_col_sums {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] [DecidableEq n] (R : Matrix m n ℝ) (hR : ∀ (i : m) (j : n), 0 ≤ R i j) {a b : ℝ} (hrow : ∀ (i : m), ∑ j : n, R i j ≤ a) (hcol : ∀ (j : n), ∑ i : m, R i j ≤ b) : ‖R‖ ≤ √(a * b)

Schur test. For a matrix R with nonnegative entries whose row sums are bounded by a and whose column sums are bounded by b, the L2 operator norm satisfies ‖R‖ ≤ sqrt (a * b). This is the "standard induced-norm inequality" ‖R‖₂ ≤ sqrt (‖R‖₁ ‖R‖∞) invoked at the end of Section 11.3 of bs_lambda.txt.