Coarse-graining support: Support.CoarseGraining.MagicIdentities.Basics

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

Foundational completed-square identities and ordering consequences.

theorem HCPolySupport.magic_vecDot_matVecMul_comm_of_isSymm {d : ℕ} {A : Mat d} (hA : Matrix.IsSymm A) (ξ η : Vec d) : vecDot ξ (matVecMul A η) = vecDot η (matVecMul A ξ)

theorem HCPolySupport.magic_half_vecDot_add_of_isSymm {d : ℕ} {A : Mat d} (hA : Matrix.IsSymm A) (ξ η : Vec d) : 1 / 2 * vecDot (ξ + η) (matVecMul A (ξ + η)) = 1 / 2 * vecDot ξ (matVecMul A ξ) + vecDot ξ (matVecMul A η) + 1 / 2 * vecDot η (matVecMul A η)

theorem HCPolySupport.magic_half_vecDot_sub_of_isSymm {d : ℕ} {A : Mat d} (hA : Matrix.IsSymm A) (ξ η : Vec d) : 1 / 2 * vecDot (ξ - η) (matVecMul A (ξ - η)) = 1 / 2 * vecDot ξ (matVecMul A ξ) - vecDot ξ (matVecMul A η) + 1 / 2 * vecDot η (matVecMul A η)

theorem HCPolySupport.magic_adjoint_shifted_square_eq_completed_square {d : ℕ} {sigma sigmaStar kappa : Mat d} (hSInvSymm : Matrix.IsSymm sigmaStar⁻¹) (hdet : IsUnit (Matrix.det sigmaStar)) (p q : Vec d) : 1 / 2 * vecDot p (matVecMul sigma p) - vecDot p q + 1 / 2 * vecDot (q - matVecMul kappa p) (matVecMul sigmaStar⁻¹ (q - matVecMul kappa p)) = 1 / 2 * vecDot p (matVecMul (sigma - sigmaStar) p) - 1 / 2 * vecDot p (matVecMul (kappa + matTranspose kappa) p) + 1 / 2 * vecDot (q - matVecMul (sigmaStar + kappa) p) (matVecMul sigmaStar⁻¹ (q - matVecMul (sigmaStar + kappa) p))

theorem HCPolySupport.magic_half_vecDot_sub_add_of_isSymm {d : ℕ} {A : Mat d} (hA : Matrix.IsSymm A) (ξ η : Vec d) : 1 / 2 * vecDot (ξ - η) (matVecMul A (ξ - η)) + 1 / 2 * vecDot (ξ + η) (matVecMul A (ξ + η)) = vecDot ξ (matVecMul A ξ) + vecDot η (matVecMul A η)

theorem HCPolySupport.magic_half_blockVecDot_neg_left_of_isSymmetricBlockMat {d : ℕ} {B : BlockMat d} (hB : IsSymmetricBlockMat B) (p q : Vec d) : 1 / 2 * blockVecDot (-p, q) (blockMatVecMul B (-p, q)) = 1 / 2 * vecDot q (matVecMul B.lowerRight q) - vecDot q (matVecMul B.lowerLeft p) + 1 / 2 * vecDot p (matVecMul B.upperLeft p)

theorem HCPolySupport.magic_half_blockVecDot_pos_left_of_isSymmetricBlockMat {d : ℕ} {B : BlockMat d} (hB : IsSymmetricBlockMat B) (p q : Vec d) : 1 / 2 * blockVecDot (p, q) (blockMatVecMul B (p, q)) = 1 / 2 * vecDot q (matVecMul B.lowerRight q) + vecDot q (matVecMul B.lowerLeft p) + 1 / 2 * vecDot p (matVecMul B.upperLeft p)

theorem HCPolySupport.magic_identity_sigmaCorrectedResponse_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) : sigmaCorrectedResponse U a p = 1 / 2 * vecDot p (matVecMul sigma p)

theorem HCPolySupport.magic_identity_responseJ_completed_square_canonical_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (p q : Vec d) : ResponseJ U p q a = sigmaCorrectedResponse U a p - vecDot p q + 1 / 2 * vecDot (q + matVecMul (kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q + matVecMul (kappaCoarse U a) p))

theorem HCPolySupport.magic_identity_responseJ_completed_square_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (p q : Vec d) : ResponseJ U p q a = 1 / 2 * vecDot p (matVecMul sigma p) - vecDot p q + 1 / 2 * vecDot (q + matVecMul kappa p) (matVecMul sigmaStar⁻¹ (q + matVecMul kappa p))

theorem HCPolySupport.magic_identity_responseJ_shifted_square_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (p q : Vec d) : ResponseJ U p q a = 1 / 2 * vecDot p (matVecMul (sigma - sigmaStar) p) + 1 / 2 * vecDot p (matVecMul (kappa + matTranspose kappa) p) + 1 / 2 * vecDot (q - matVecMul (sigmaStar - kappa) p) (matVecMul sigmaStar⁻¹ (q - matVecMul (sigmaStar - kappa) p))

theorem HCPolySupport.magic_identity_responseJ_shifted_square_canonical_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (p q : Vec d) : ResponseJ U p q a = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p) + 1 / 2 * vecDot p (matVecMul (kappaCoarse U a + matTranspose (kappaCoarse U a)) p) + 1 / 2 * vecDot (q - matVecMul (sigmaStarCoarse U a - kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (sigmaStarCoarse U a - kappaCoarse U a) p))

theorem HCPolySupport.magic_identity_responseJ_adjoint_completed_square_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hK : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigma : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p q : Vec d) : ResponseJ U p q (adjointCoeffField a) = 1 / 2 * vecDot p (matVecMul sigma p) - vecDot p q + 1 / 2 * vecDot (q - matVecMul kappa p) (matVecMul sigmaStar⁻¹ (q - matVecMul kappa p))

theorem HCPolySupport.magic_identity_responseJ_adjoint_shifted_square_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hK : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigma : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p q : Vec d) : ResponseJ U p q (adjointCoeffField a) = 1 / 2 * vecDot p (matVecMul (sigma - sigmaStar) p) - 1 / 2 * vecDot p (matVecMul (kappa + matTranspose kappa) p) + 1 / 2 * vecDot (q - matVecMul (sigmaStar + kappa) p) (matVecMul sigmaStar⁻¹ (q - matVecMul (sigmaStar + kappa) p))

theorem HCPolySupport.magic_identity_responseJ_adjoint_sum_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p q h : Vec d) : ResponseJ U p (q - h) a + ResponseJ U p (q + h) (adjointCoeffField a) = vecDot p (matVecMul (sigma - sigmaStar) p) + vecDot (q - matVecMul sigmaStar p) (matVecMul sigmaStar⁻¹ (q - matVecMul sigmaStar p)) + vecDot (h - matVecMul kappa p) (matVecMul sigmaStar⁻¹ (h - matVecMul kappa p))

theorem HCPolySupport.magic_identity_responseJ_adjoint_sum_canonical_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p q h : Vec d) : ResponseJ U p (q - h) a + ResponseJ U p (q + h) (adjointCoeffField a) = vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p) + vecDot (q - matVecMul (sigmaStarCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (sigmaStarCoarse U a) p)) + vecDot (h - matVecMul (kappaCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (h - matVecMul (kappaCoarse U a) p))

theorem HCPolySupport.magic_identity_responseJ_adjoint_diagonal_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) : ResponseJ U p (matVecMul (sigmaStar - kappa) p) a + ResponseJ U p (matVecMul (sigmaStar + kappa) p) (adjointCoeffField a) = vecDot p (matVecMul (sigma - sigmaStar) p)

theorem HCPolySupport.magic_identity_responseJ_adjoint_diagonal_canonical_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) : ResponseJ U p (matVecMul (sigmaStarCoarse U a - kappaCoarse U a) p) a + ResponseJ U p (matVecMul (sigmaStarCoarse U a + kappaCoarse U a) p) (adjointCoeffField a) = vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p)

theorem HCPolySupport.magic_identity_responseJ_sigmaStar_sub_kappa_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) : ResponseJ U p (matVecMul (sigmaStar - kappa) p) a = 1 / 2 * vecDot p (matVecMul (sigma - sigmaStar) p) + 1 / 2 * vecDot p (matVecMul (kappa + matTranspose kappa) p)

theorem HCPolySupport.magic_identity_responseJ_sigmaStar_sub_kappa_canonical_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) : ResponseJ U p (matVecMul (sigmaStarCoarse U a - kappaCoarse U a) p) a = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p) + 1 / 2 * vecDot p (matVecMul (kappaCoarse U a + matTranspose (kappaCoarse U a)) p)

theorem HCPolySupport.magic_identity_responseJ_adjoint_sigmaStar_add_kappa_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) : ResponseJ U p (matVecMul (sigmaStar + kappa) p) (adjointCoeffField a) = 1 / 2 * vecDot p (matVecMul (sigma - sigmaStar) p) - 1 / 2 * vecDot p (matVecMul (kappa + matTranspose kappa) p)

theorem HCPolySupport.sigmaStar_le_sigma_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) : vecDot p (matVecMul sigmaStar p) ≤ vecDot p (matVecMul sigma p)

theorem HCPolySupport.sigmaStarCoarse_le_sigmaCoarse_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) : vecDot p (matVecMul (sigmaStarCoarse U a) p) ≤ vecDot p (matVecMul (sigmaCoarse U a) p)

theorem HCPolySupport.kappa_add_transpose_le_sigma_sub_sigmaStar_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) : vecDot p (matVecMul (kappa + matTranspose kappa) p) ≤ vecDot p (matVecMul (sigma - sigmaStar) p)

theorem HCPolySupport.neg_kappa_add_transpose_le_sigma_sub_sigmaStar_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) : -vecDot p (matVecMul (kappa + matTranspose kappa) p) ≤ vecDot p (matVecMul (sigma - sigmaStar) p)

theorem HCPolySupport.kappaCoarse_add_transpose_le_sigmaCoarse_sub_sigmaStarCoarse_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) : vecDot p (matVecMul (kappaCoarse U a + matTranspose (kappaCoarse U a)) p) ≤ vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p)

theorem HCPolySupport.neg_kappaCoarse_add_transpose_le_sigmaCoarse_sub_sigmaStarCoarse_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) : -vecDot p (matVecMul (kappaCoarse U a + matTranspose (kappaCoarse U a)) p) ≤ vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p)

theorem HCPolySupport.basic_cg_identities_coarse_graining_canonical_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p (matVecMul (sigmaStarCoarse U a - kappaCoarse U a) p) a u) (w : AHarmonicFunction a U) : |(volumeAverage U fun (x : Vec d) => vecDot (matVecMul (sigmaStarCoarse U a - kappaCoarse U a) p) (w.toH1.grad x)) - volumeAverage U fun (x : Vec d) => vecDot p (matVecMul (a x) (w.toH1.grad x))| ≤ √(volumeAverage U (scalarVariationEnergyIntegrand a w)) * √(2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p))

theorem HCPolySupport.basic_cg_identities_coarse_graining_canonical_of_isSigmaCoarse_of_isEllipticFieldOn {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p (matVecMul (sigmaStarCoarse U a - kappaCoarse U a) p) a u) (w : AHarmonicFunction a U) : |(volumeAverage U fun (x : Vec d) => vecDot (matVecMul (sigmaStarCoarse U a - kappaCoarse U a) p) (w.toH1.grad x)) - volumeAverage U fun (x : Vec d) => vecDot p (matVecMul (a x) (w.toH1.grad x))| ≤ √(volumeAverage U (scalarVariationEnergyIntegrand a w)) * √(2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p))

theorem HCPolySupport.basic_cg_identities_coarse_graining_average_pairing_canonical_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p (matVecMul (sigmaStarCoarse U a - kappaCoarse U a) p) a u) (w : AHarmonicFunction a U) : |vecDot p (matVecMul (aStarCoarse (sigmaStarCoarse U a) (kappaCoarse U a)) fun (i : Fin d) => volumeAverage U fun (x : Vec d) => w.toH1.grad x i) - vecDot p fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x) i| ≤ √(volumeAverage U (scalarVariationEnergyIntegrand a w)) * √(2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p))

theorem HCPolySupport.averagePairingCanonical_of_sigmaCoarse_and_ellipticity {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p (matVecMul (sigmaStarCoarse U a - kappaCoarse U a) p) a u) (w : AHarmonicFunction a U) : |vecDot p (matVecMul (aStarCoarse (sigmaStarCoarse U a) (kappaCoarse U a)) fun (i : Fin d) => volumeAverage U fun (x : Vec d) => w.toH1.grad x i) - vecDot p fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x) i| ≤ √(volumeAverage U (scalarVariationEnergyIntegrand a w)) * √(2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p))

theorem HCPolySupport.basic_cg_identities_coarse_graining_average_difference_canonical_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) (hInt : ResponseLinearIntegrabilityData U a) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p (matVecMul (sigmaStarCoarse U a - kappaCoarse U a) p) a u) (w : AHarmonicFunction a U) : |vecDot p ((matVecMul (aStarCoarse (sigmaStarCoarse U a) (kappaCoarse U a)) fun (i : Fin d) => volumeAverage U fun (x : Vec d) => w.toH1.grad x i) - fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x) i)| ≤ √(volumeAverage U (scalarVariationEnergyIntegrand a w)) * √(2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p))

theorem HCPolySupport.basic_cg_identities_coarse_graining_average_difference_canonical {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar) (hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa)) (hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa)) (hdet : IsUnit (Matrix.det sigmaStar)) (p : Vec d) (u : AHarmonicFunction a U) (hmax : IsResponseMaximizer U p (matVecMul (sigmaStarCoarse U a - kappaCoarse U a) p) a u) (w : AHarmonicFunction a U) : |vecDot p ((matVecMul (aStarCoarse (sigmaStarCoarse U a) (kappaCoarse U a)) fun (i : Fin d) => volumeAverage U fun (x : Vec d) => w.toH1.grad x i) - fun (i : Fin d) => volumeAverage U fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x) i)| ≤ √(volumeAverage U (scalarVariationEnergyIntegrand a w)) * √(2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p))