Coarse-graining support: Support.Deterministic.CoarsePoincare.Setup.EnergyControls

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

theorem HCPolySupport.abs_vecDot_matVecMul_le_matNorm_mul_vecNormSq {d : ℕ} (A : Mat d) (x : Vec d) : |vecDot x (matVecMul A x)| ≤ matNorm A * vecNormSq x

theorem HCPolySupport.vecDot_matVecMul_le_matNorm_mul_vecNormSq_of_posSemidef {d : ℕ} {A : Mat d} (hA : Matrix.PosSemidef A) (x : Vec d) : vecDot x (matVecMul A x) ≤ matNorm A * vecNormSq x

theorem HCPolySupport.vecNormSq_le_matNorm_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 ξ ≤ matNorm B * vecDot ξ (matVecMul A ξ)