High-contrast homogenization: Entry.Geometry.QuadraticForm

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Quadratic forms and the Euclidean operator norm

The matrix analysis behind e.rounded.grid.bounds is carried out entirely with quadratic forms v ⬝ᵥ (M *ᵥ v) and squared Euclidean norms vecNormSq. This file provides:

• the symmetric-form identities and the Cauchy–Schwarz inequality for a positive semidefinite form, (x ⬝ᵥ M y)² ≤ (x ⬝ᵥ M x)(y ⬝ᵥ M y);
• the bridge between Mathlib's L2 operator norm ‖M‖ (the print's |M|) and the vector form |M v|² ≤ ‖M‖² |v|², in both directions;
• two consequences for a symmetric positive semidefinite M: a bound ⟨v, M v⟩ ≤ K |v|² on the form upgrades to |M v| ≤ K |v|, and c |v|² ≤ ⟨v, M v⟩ upgrades to c |v| ≤ |M v|.

The print's |·| on matrices is the Euclidean operator norm; Mathlib's scoped instance Matrix.Norms.L2Operator is exactly that norm, and every use of it below goes through the single inequality Matrix.l2_opNorm_mulVec.

Symmetric forms

theorem HCPolySupport.HighContrast.Geometry.vecNormSq_eq_dotProduct {d : ℕ} (v : Vec d) : vecNormSq v = v ⬝ᵥ v

theorem HCPolySupport.HighContrast.Geometry.transpose_eq_of_isHermitian {d : ℕ} {M : Mat d} (hM : Matrix.IsHermitian M) : Matrix.transpose M = M

theorem HCPolySupport.HighContrast.Geometry.dotProduct_mulVec_nonneg_of_posSemidef {d : ℕ} {M : Mat d} (hM : Matrix.PosSemidef M) (x : Vec d) : 0 ≤ x ⬝ᵥ Matrix.mulVec M x

theorem HCPolySupport.HighContrast.Geometry.dotProduct_mulVec_comm {d : ℕ} {M : Mat d} (hM : Matrix.transpose M = M) (x y : Vec d) : x ⬝ᵥ Matrix.mulVec M y = y ⬝ᵥ Matrix.mulVec M x

The form of a symmetric matrix is symmetric.

theorem HCPolySupport.HighContrast.Geometry.vecNormSq_mulVec_eq {d : ℕ} {M : Mat d} (hM : Matrix.transpose M = M) (v : Vec d) : vecNormSq (Matrix.mulVec M v) = v ⬝ᵥ (M * M).mulVec v

For symmetric M, |M v|² = ⟨v, M² v⟩.

theorem HCPolySupport.HighContrast.Geometry.sq_dotProduct_mulVec_le {d : ℕ} {M : Mat d} (hM : Matrix.transpose M = M) (hpos : ∀ (x : Vec d), 0 ≤ x ⬝ᵥ Matrix.mulVec M x) (x y : Vec d) : (x ⬝ᵥ Matrix.mulVec M y) ^ 2 ≤ x ⬝ᵥ Matrix.mulVec M x * y ⬝ᵥ Matrix.mulVec M y

Cauchy–Schwarz for a positive semidefinite form.

The operator norm bridge

theorem HCPolySupport.HighContrast.Geometry.norm_toLp_sq {d : ℕ} (v : Vec d) : ‖WithLp.toLp 2 v‖ ^ 2 = vecNormSq v

theorem HCPolySupport.HighContrast.Geometry.vecNormSq_mulVec_le_opNorm {d : ℕ} (M : Mat d) (v : Vec d) : vecNormSq (Matrix.mulVec M v) ≤ ‖M‖ ^ 2 * vecNormSq v

|M v|² ≤ ‖M‖² |v|² for the Euclidean operator norm.

theorem HCPolySupport.HighContrast.Geometry.opNorm_le_of_vecNormSq_mulVec_le {d : ℕ} {M : Mat d} {K : ℝ} (hK : 0 ≤ K) (h : ∀ (v : Vec d), vecNormSq (Matrix.mulVec M v) ≤ K ^ 2 * vecNormSq v) : ‖M‖ ≤ K

The converse: a uniform bound |M v|² ≤ K² |v|² bounds the operator norm.

Form bounds from vector bounds and back

theorem HCPolySupport.HighContrast.Geometry.abs_dotProduct_mulVec_le_of_vecNormSq_le {d : ℕ} {M : Mat d} {K : ℝ} (hK : 0 ≤ K) (h : ∀ (v : Vec d), vecNormSq (Matrix.mulVec M v) ≤ K ^ 2 * vecNormSq v) (v : Vec d) : |v ⬝ᵥ Matrix.mulVec M v| ≤ K * vecNormSq v

A vector bound |M v| ≤ K |v| bounds the form: |⟨v, M v⟩| ≤ K |v|².

theorem HCPolySupport.HighContrast.Geometry.dotProduct_mulVec_le_opNorm {d : ℕ} (M : Mat d) (v : Vec d) : v ⬝ᵥ Matrix.mulVec M v ≤ ‖M‖ * vecNormSq v

⟨v, M v⟩ ≤ ‖M‖ |v|².

theorem HCPolySupport.HighContrast.Geometry.dotProduct_mulVec_le_sqrt_opNorm_sq {d : ℕ} {R P : Mat d} (hR : Matrix.transpose R = R) (hRP : R * R = P) (u : Vec d) : u ⬝ᵥ Matrix.mulVec R u ≤ √‖P‖ * vecNormSq u

For a symmetric matrix R with R * R = P: ⟨u, R u⟩ ≤ √‖P‖ |u|².

theorem HCPolySupport.HighContrast.Geometry.vecNormSq_mulVec_le_of_dotProduct_le {d : ℕ} {M : Mat d} (hM : Matrix.transpose M = M) (hpos : ∀ (x : Vec d), 0 ≤ x ⬝ᵥ Matrix.mulVec M x) {K : ℝ} (hK : 0 ≤ K) (h : ∀ (x : Vec d), x ⬝ᵥ Matrix.mulVec M x ≤ K * vecNormSq x) (v : Vec d) : vecNormSq (Matrix.mulVec M v) ≤ K ^ 2 * vecNormSq v

For a symmetric positive semidefinite M, a bound ⟨x, M x⟩ ≤ K |x|² on the form gives the vector bound |M v|² ≤ K² |v|².

theorem HCPolySupport.HighContrast.Geometry.vecNormSq_le_vecNormSq_mulVec_of_le_dotProduct {d : ℕ} {M : Mat d} {c : ℝ} (hc : 0 ≤ c) (h : ∀ (x : Vec d), c * vecNormSq x ≤ x ⬝ᵥ Matrix.mulVec M x) (v : Vec d) : c ^ 2 * vecNormSq v ≤ vecNormSq (Matrix.mulVec M v)

A lower bound c |x|² ≤ ⟨x, M x⟩ on the form gives c² |v|² ≤ |M v|².