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

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

structure HCPolySupport.Book.Ch02.ResponseQuadraticTheory {d : ℕ} (U : Domain d) (a : CoeffOn U) : Prop

Public theorem package for the statement that (p,q) ↦ J(U,p,q;a) is quadratic.

The two fields are the homogeneity and parallelogram identities. The canonical public theorem proving this package is responseQuadraticTheory in Quadraticity.lean.

• responseJ_smul (c : ℝ) (p q : Vec d) : responseJ U a (c • p) (c • q) = c ^ 2 * responseJ U a p q
• responseJ_parallelogram (p1 q1 p2 q2 : Vec d) : responseJ U a (p1 + p2) (q1 + q2) + responseJ U a (p1 - p2) (q1 - q2) = 2 * responseJ U a p1 q1 + 2 * responseJ U a p2 q2

theorem HCPolySupport.Book.Ch02.ResponseQuadraticTheory.ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (hQuad : ResponseQuadraticTheory U a) : ResponseQuadraticTheory U b

theorem HCPolySupport.Book.Ch02.ResponseQuadraticTheory.iff_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : ResponseQuadraticTheory U a ↔ ResponseQuadraticTheory U b

theorem HCPolySupport.Book.Ch02.responseJ_smul_of_responseQuadraticTheory {d : ℕ} {U : Domain d} {a : CoeffOn U} (hQuad : ResponseQuadraticTheory U a) (c : ℝ) (p q : Vec d) : responseJ U a (c • p) (c • q) = c ^ 2 * responseJ U a p q

theorem HCPolySupport.Book.Ch02.responseJ_parallelogram_of_responseQuadraticTheory {d : ℕ} {U : Domain d} {a : CoeffOn U} (hQuad : ResponseQuadraticTheory U a) (p1 q1 p2 q2 : Vec d) : responseJ U a (p1 + p2) (q1 + q2) + responseJ U a (p1 - p2) (q1 - q2) = 2 * responseJ U a p1 q1 + 2 * responseJ U a p2 q2