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

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

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

Public theorem package for the first-variation theorem.

This is not a definition of maximizer; it is the proposition-valued package proved by responseFirstVariationTheory in FirstVariation.lean. Downstream note-facing wrappers should use that theorem rather than carry this package as an additional input.

• first_variation (p q : Vec d) (v : Solution U a) : IsResponseMaximizer U a p q v → ∀ (w : Solution U a), firstVariationValue U a p q v w = 0

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

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

theorem HCPolySupport.Book.Ch02.firstVariationValue_eq_zero_of_isResponseMaximizer {d : ℕ} {U : Domain d} {a : CoeffOn U} (hFirst : ResponseFirstVariationTheory U a) {p q : Vec d} {v : Solution U a} (hv : IsResponseMaximizer U a p q v) (w : Solution U a) : firstVariationValue U a p q v w = 0

theorem HCPolySupport.Book.Ch02.canonicalMaximizer_firstVariationValue_eq_zero {d : ℕ} {U : Domain d} {a : CoeffOn U} (hTheory : ResponseExistenceTheory U a) (hFirst : ResponseFirstVariationTheory U a) (p q : Vec d) (w : Solution U a) : firstVariationValue U a p q (canonicalMaximizer hTheory p q).toSolution w = 0