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

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

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

Public theorem package for uniqueness of the response maximizer gradient.

The statement is deliberately a.e. in the gradient. A later Poincare argument can upgrade this to uniqueness of the mean-zero representative. The canonical public theorem proving this package is responseGradientUniquenessTheory in GradientUniqueness.lean.

• unique_gradient (p q : Vec d) (v w : Solution U a) : IsResponseMaximizer U a p q v → IsResponseMaximizer U a p q w → v.SameGradientAE w

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

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

theorem HCPolySupport.Book.Ch02.sameGradientAE_of_response_maximizers {d : ℕ} {U : Domain d} {a : CoeffOn U} (hUnique : ResponseGradientUniquenessTheory U a) {p q : Vec d} {v w : Solution U a} (hv : IsResponseMaximizer U a p q v) (hw : IsResponseMaximizer U a p q w) : v.SameGradientAE w

theorem HCPolySupport.Book.Ch02.canonicalMaximizer_sameGradientAE {d : ℕ} {U : Domain d} {a : CoeffOn U} (hTheory : ResponseExistenceTheory U a) (hUnique : ResponseGradientUniquenessTheory U a) {p q : Vec d} {v : Solution U a} (hv : IsResponseMaximizer U a p q v) : (canonicalMaximizer hTheory p q).toSolution.SameGradientAE v