Coarse-graining support: Support.CoarseGraining.BlockFormalism.EllipticBounds

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

Block formalism -- symmetric and elliptic matrix bounds

Symmetric block-matrix identities, symmPartInv lower / upper bound and positivity under IsEllipticMatrix, blockMatrixOfCoeff_half_quadratic_ge_vecDot, blockMatrixOfCoeff_quadratic positivity / lower / upper / plainUpperBound, coercivity, and the image bounds used by the response functional.

theorem HCPolySupport.blockMatrixOfCoeff_upperLeft_isSymm {d : ℕ} (A : Mat d) : matTranspose (blockMatrixOfCoeff A).upperLeft = (blockMatrixOfCoeff A).upperLeft

theorem HCPolySupport.blockMatrixOfCoeff_upperRight_transpose {d : ℕ} (A : Mat d) : matTranspose (blockMatrixOfCoeff A).upperRight = (blockMatrixOfCoeff A).lowerLeft

theorem HCPolySupport.blockMatrixOfCoeff_lowerRight_isSymm {d : ℕ} (A : Mat d) : matTranspose (blockMatrixOfCoeff A).lowerRight = (blockMatrixOfCoeff A).lowerRight

theorem HCPolySupport.isSymm_toFullBlockMat_of_isSymmetricBlockMat {d : ℕ} {B : BlockMat d} (hB : IsSymmetricBlockMat B) : Matrix.IsSymm (toFullBlockMat B)

theorem HCPolySupport.blockVecDot_blockMatVecMul_comm_of_isSymmetricBlockMat {d : ℕ} {B : BlockMat d} (hB : IsSymmetricBlockMat B) (X Y : BlockVec d) : blockVecDot X (blockMatVecMul B Y) = blockVecDot Y (blockMatVecMul B X)

theorem HCPolySupport.isSymmetricBlockMat_blockMatrixOfCoeff {d : ℕ} (A : Mat d) : IsSymmetricBlockMat (blockMatrixOfCoeff A)

theorem HCPolySupport.blockVecDot_blockMatVecMul_blockMatrixOfCoeff_comm {d : ℕ} (A : Mat d) (X Y : BlockVec d) : blockVecDot X (blockMatVecMul (blockMatrixOfCoeff A) Y) = blockVecDot Y (blockMatVecMul (blockMatrixOfCoeff A) X)

theorem HCPolySupport.isUnit_symmPart_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) : IsUnit (symmPart A)

theorem HCPolySupport.symmPart_inv_nonneg_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (ξ : Vec d) : 0 ≤ vecDot ξ (matVecMul (symmPart A)⁻¹ ξ)

theorem HCPolySupport.lowerBound_symmPartInv_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (ξ : Vec d) : lam * (Lam⁻¹ * Lam⁻¹) * vecNormSq ξ ≤ vecDot ξ (matVecMul (symmPart A)⁻¹ ξ)

theorem HCPolySupport.vecNormSq_matVecMul_symmPartInv_le_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (ξ : Vec d) : vecNormSq (matVecMul (symmPart A)⁻¹ ξ) ≤ lam⁻¹ * lam⁻¹ * vecNormSq ξ

theorem HCPolySupport.symmPart_inv_upperBound_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (ξ : Vec d) : vecDot ξ (matVecMul (symmPart A)⁻¹ ξ) ≤ lam⁻¹ * vecNormSq ξ

theorem HCPolySupport.vecDot_matVecMul_skewPart_self_eq_zero {d : ℕ} (A : Mat d) (p : Vec d) : vecDot p (matVecMul (skewPart A) p) = 0

theorem HCPolySupport.blockMatrixOfCoeff_half_quadratic_ge_vecDot_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (p q : Vec d) : vecDot p q ≤ 1 / 2 * blockVecDot (p, q) (blockMatVecMul (blockMatrixOfCoeff A) (p, q))

theorem HCPolySupport.blockMatrixOfCoeff_quadratic_pos_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} {p q : Vec d} (hA : IsEllipticMatrix lam Lam A) (hpq : (p, q) ≠ 0) : 0 < blockVecDot (p, q) (blockMatVecMul (blockMatrixOfCoeff A) (p, q))

theorem HCPolySupport.blockMatrixOfCoeff_quadratic_lowerBound_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (p q : Vec d) : lam / (1 + 2 * Lam ^ 2) * blockVecDot (p, q) (p, q) ≤ blockVecDot (p, q) (blockMatVecMul (blockMatrixOfCoeff A) (p, q))

theorem HCPolySupport.blockMatrixOfCoeff_coercive_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (X : BlockVec d) : lam / (1 + 2 * Lam ^ 2) * blockVecDot X X ≤ blockVecDot X (blockMatVecMul (blockMatrixOfCoeff A) X)

theorem HCPolySupport.blockMatrixOfCoeff_quadratic_upperBound_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (p q : Vec d) : blockVecDot (p, q) (blockMatVecMul (blockMatrixOfCoeff A) (p, q)) ≤ Lam * vecNormSq p + lam⁻¹ * vecNormSq (q - matVecMul (skewPart A) p)

theorem HCPolySupport.blockMatrixOfCoeff_quadratic_plainUpperBound_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (p q : Vec d) : blockVecDot (p, q) (blockMatVecMul (blockMatrixOfCoeff A) (p, q)) ≤ (Lam + 2 * lam⁻¹ * Lam ^ 2) * vecNormSq p + 2 * lam⁻¹ * vecNormSq q

theorem HCPolySupport.blockMatVecMul_blockMatrixOfCoeff_snd_recover_flux_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (p q : Vec d) : q = matVecMul (symmPart A) (blockMatVecMul (blockMatrixOfCoeff A) (p, q)).2 + matVecMul (skewPart A) p

theorem HCPolySupport.blockMatrixOfCoeff_image_plainUpperBound_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (p q : Vec d) : blockVecDot (blockMatVecMul (blockMatrixOfCoeff A) (p, q)) (blockMatVecMul (blockMatrixOfCoeff A) (p, q)) ≤ (2 * Lam ^ 2 + 2 * (2 * Lam ^ 2 + 1) * (lam⁻¹ * lam⁻¹) * Lam ^ 2) * vecNormSq p + 2 * (2 * Lam ^ 2 + 1) * (lam⁻¹ * lam⁻¹) * vecNormSq q

noncomputable def HCPolySupport.blockMatrixOfCoeffNormSqBound (lam Lam : ℝ) : ℝ

An explicit squared operator-norm bound for the block matrix induced by a coefficient matrix with ellipticity parameters lam and Lam.

Equations

• HCPolySupport.blockMatrixOfCoeffNormSqBound lam Lam = 2 * Lam ^ 2 + 2 * (2 * Lam ^ 2 + 1) * (lam⁻¹ * lam⁻¹) * (Lam ^ 2 + 1)

theorem HCPolySupport.blockMatrixOfCoeff_image_bound_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (X : BlockVec d) : blockVecDot (blockMatVecMul (blockMatrixOfCoeff A) X) (blockMatVecMul (blockMatrixOfCoeff A) X) ≤ blockMatrixOfCoeffNormSqBound lam Lam * blockVecDot X X