Coarse-graining support: Support.Book.Ch02.Theorems.MatrixOperatorNorm

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Operator Norm API for Chapter 2 Matrices

This file gives the reusable Euclidean operator-norm API used by the public Chapter 2 multiscale ellipticity definitions. The explicitly named Frobenius norm below is retained only as compatibility infrastructure for older deterministic estimates.

noncomputable def HCPolySupport.Book.Ch02.matrixOperatorNorm {d : ℕ} (A : Mat d) : ℝ

Euclidean/L2 operator norm of a square real matrix, viewed as an operator on finite-dimensional Euclidean space.

Equations

• HCPolySupport.Book.Ch02.matrixOperatorNorm A = ‖Matrix.toEuclideanCLM A‖

def HCPolySupport.Book.Ch02.matrixFrobeniusNormSq {d : ℕ} (A : Mat d) : ℝ

Legacy Frobenius squared norm, kept under an explicit compatibility name.

Equations

• HCPolySupport.Book.Ch02.matrixFrobeniusNormSq A = ∑ i : Fin d, ∑ j : Fin d, A i j ^ 2

noncomputable def HCPolySupport.Book.Ch02.matrixFrobeniusNorm {d : ℕ} (A : Mat d) : ℝ

Legacy Frobenius norm, kept under an explicit compatibility name.

Equations

• HCPolySupport.Book.Ch02.matrixFrobeniusNorm A = √(HCPolySupport.Book.Ch02.matrixFrobeniusNormSq A)

noncomputable def HCPolySupport.Book.Ch02.vecNorm {d : ℕ} (x : Vec d) : ℝ

Euclidean/L2 norm of a vector, compatible with the project's vecNormSq.

Equations

• HCPolySupport.Book.Ch02.vecNorm x = ‖WithLp.toLp 2 x‖

theorem HCPolySupport.Book.Ch02.matrixOperatorNorm_eq_l2_opNorm {d : ℕ} (A : Mat d) : matrixOperatorNorm A = ‖A‖

theorem HCPolySupport.Book.Ch02.matrixOperatorNorm_nonneg {d : ℕ} (A : Mat d) : 0 ≤ matrixOperatorNorm A

@[simp]

theorem HCPolySupport.Book.Ch02.matrixOperatorNorm_zero {d : ℕ} : matrixOperatorNorm 0 = 0

@[simp]

theorem HCPolySupport.Book.Ch02.matrixOperatorNorm_one {d : ℕ} [NeZero d] : matrixOperatorNorm 1 = 1

theorem HCPolySupport.Book.Ch02.matrixOperatorNorm_mul_le {d : ℕ} (A B : Mat d) : matrixOperatorNorm (A * B) ≤ matrixOperatorNorm A * matrixOperatorNorm B

theorem HCPolySupport.Book.Ch02.norm_toEuclideanCLM_reindex_self {n : Type u_1} [Fintype n] [DecidableEq n] (e : n ≃ n) (M : Matrix n n ℝ) : ‖Matrix.toEuclideanCLM ((Matrix.reindex e e) M)‖ = ‖Matrix.toEuclideanCLM M‖

Reindexing both coordinates by the same equivalence preserves the Euclidean operator norm.

theorem HCPolySupport.Book.Ch02.matrixOperatorNorm_inv_le_of_mul_eq_one {d : ℕ} [NeZero d] {A B : Mat d} (hAB : A * B = 1) (hApos : 0 < matrixOperatorNorm A) : (matrixOperatorNorm A)⁻¹ ≤ matrixOperatorNorm B

theorem HCPolySupport.Book.Ch02.matrixOperatorNorm_diagonal {d : ℕ} (v : Fin d → ℝ) : matrixOperatorNorm (Matrix.diagonal v) = ‖v‖

theorem HCPolySupport.Book.Ch02.matrixOperatorNorm_smul_one_eq_abs {d : ℕ} [NeZero d] (σ : ℝ) : matrixOperatorNorm (σ • 1) = |σ|

theorem HCPolySupport.Book.Ch02.matrixOperatorNorm_smul_one_eq_of_nonneg {d : ℕ} [NeZero d] {σ : ℝ} (hσ : 0 ≤ σ) : matrixOperatorNorm (σ • 1) = σ

theorem HCPolySupport.Book.Ch02.matrixFrobeniusNormSq_nonneg {d : ℕ} (A : Mat d) : 0 ≤ matrixFrobeniusNormSq A

theorem HCPolySupport.Book.Ch02.matrixFrobeniusNorm_nonneg {d : ℕ} (A : Mat d) : 0 ≤ matrixFrobeniusNorm A

theorem HCPolySupport.Book.Ch02.vecNorm_nonneg {d : ℕ} (x : Vec d) : 0 ≤ vecNorm x

theorem HCPolySupport.Book.Ch02.vecNorm_sq_eq_vecNormSq {d : ℕ} (x : Vec d) : vecNorm x ^ 2 = vecNormSq x

theorem HCPolySupport.Book.Ch02.vecNormSq_matVecMul_le_matrixFrobeniusNormSq_mul_vecNormSq {d : ℕ} (A : Mat d) (x : Vec d) : vecNormSq (matVecMul A x) ≤ matrixFrobeniusNormSq A * vecNormSq x

theorem HCPolySupport.Book.Ch02.vecNorm_matVecMul_le_matrixOperatorNorm_mul_vecNorm {d : ℕ} (A : Mat d) (x : Vec d) : vecNorm (matVecMul A x) ≤ matrixOperatorNorm A * vecNorm x

theorem HCPolySupport.Book.Ch02.vecNormSq_matVecMul_le_matrixOperatorNorm_sq_mul_vecNormSq {d : ℕ} (A : Mat d) (x : Vec d) : vecNormSq (matVecMul A x) ≤ matrixOperatorNorm A ^ 2 * vecNormSq x

theorem HCPolySupport.Book.Ch02.matrixOperatorNorm_le_matrixFrobeniusNorm {d : ℕ} (A : Mat d) : matrixOperatorNorm A ≤ matrixFrobeniusNorm A

theorem HCPolySupport.Book.Ch02.abs_entry_le_matrixOperatorNorm {d : ℕ} (A : Mat d) (i j : Fin d) : |A i j| ≤ matrixOperatorNorm A

theorem HCPolySupport.Book.Ch02.matrixFrobeniusNorm_le_dim_mul_matrixOperatorNorm {d : ℕ} (A : Mat d) : matrixFrobeniusNorm A ≤ ↑d * matrixOperatorNorm A

In finite dimension the legacy Frobenius norm is controlled by d times the Euclidean operator norm. This is the compatibility direction used when old deterministic Frobenius estimates are retained as proof infrastructure.

theorem HCPolySupport.Book.Ch02.matrixFrobeniusNorm_le_sum_abs_entries {d : ℕ} (A : Mat d) : matrixFrobeniusNorm A ≤ ∑ i : Fin d, ∑ j : Fin d, |A i j|

The legacy Frobenius norm is bounded by the entrywise l¹ norm.

theorem HCPolySupport.Book.Ch02.matrixOperatorNorm_le_matrixOperatorNorm_add_matrixOperatorNorm_sub {d : ℕ} (A B : Mat d) : matrixOperatorNorm A ≤ matrixOperatorNorm B + matrixOperatorNorm (A - B)

Triangle inequality for the Euclidean operator norm around a matrix center.

theorem HCPolySupport.Book.Ch02.matrixOperatorNorm_le_matrixOperatorNorm_add_sum_abs_sub_entries {d : ℕ} (A B : Mat d) : matrixOperatorNorm A ≤ matrixOperatorNorm B + ∑ i : Fin d, ∑ j : Fin d, |A i j - B i j|

The Euclidean operator norm around a center is controlled by the entrywise l¹ size of the centered matrix.

theorem HCPolySupport.Book.Ch02.abs_vecDot_le_vecNorm_mul_vecNorm {d : ℕ} (x y : Vec d) : |vecDot x y| ≤ vecNorm x * vecNorm y

theorem HCPolySupport.Book.Ch02.abs_vecDot_matVecMul_le_matrixOperatorNorm_mul_vecNormSq {d : ℕ} (A : Mat d) (x : Vec d) : |vecDot x (matVecMul A x)| ≤ matrixOperatorNorm A * vecNormSq x

theorem HCPolySupport.Book.Ch02.vecDot_matVecMul_le_matrixOperatorNorm_mul_vecNormSq_of_posSemidef {d : ℕ} {A : Mat d} (hA : Matrix.PosSemidef A) (x : Vec d) : vecDot x (matVecMul A x) ≤ matrixOperatorNorm A * vecNormSq x

theorem HCPolySupport.Book.Ch02.vecNormSq_le_matrixOperatorNorm_mul_vecDot_matVecMul_of_posSemidef_of_leftInverse {d : ℕ} {A B : Mat d} (hB : Matrix.PosSemidef B) (hleftInv : ∀ (ξ : Vec d), matVecMul B (matVecMul A ξ) = ξ) (ξ : Vec d) : vecNormSq ξ ≤ matrixOperatorNorm B * vecDot ξ (matVecMul A ξ)

theorem HCPolySupport.Book.Ch02.vecNormSq_matVecMul_le_matrixOperatorNorm_sq_mul_vecNormSq_of_matLoewnerLE {d : ℕ} {A B : Mat d} (hA : Matrix.PosSemidef A) (hB : Matrix.PosSemidef B) (hAB : MatLoewnerLE A B) (x : Vec d) : vecNormSq (matVecMul A x) ≤ matrixOperatorNorm B ^ 2 * vecNormSq x

theorem HCPolySupport.Book.Ch02.matrixOperatorNorm_le_of_matLoewnerLE_of_posSemidef {d : ℕ} {A B : Mat d} (hA : Matrix.PosSemidef A) (hB : Matrix.PosSemidef B) (hAB : MatLoewnerLE A B) : matrixOperatorNorm A ≤ matrixOperatorNorm B

theorem HCPolySupport.Book.Ch02.matrixOperatorNorm_pos_of_posDef {d : ℕ} [NeZero d] {A : Mat d} (hA : Matrix.PosDef A) : 0 < matrixOperatorNorm A

theorem HCPolySupport.Book.Ch02.matrixOperatorNorm_descendantsAverageMat_le_descendantsAverage {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → Mat d) : matrixOperatorNorm (descendantsAverageMat Q j F) ≤ descendantsAverage Q j fun (R : TriadicCube d) => matrixOperatorNorm (F R)