Quadraticity

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

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

Public Chapter 2 quadraticity theorem for the response functional.

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

Public homogeneity identity for the response functional.

theorem HCPolySupport.Book.Ch02.responseJ_parallelogram {d : ℕ} {U : Domain d} {a : CoeffOn U} (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

Public parallelogram identity for the response functional.