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

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

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

Public Chapter 2 a.e. uniqueness theorem for response-maximizer gradients.

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

Public a.e. gradient uniqueness for response maximizers with the same loading.

theorem HCPolySupport.Book.Ch02.canonicalMaximizer_sameGradientAE_of_isResponseMaximizer {d : ℕ} {U : Domain d} {a : CoeffOn U} {p q : Vec d} {v : Solution U a} (hv : IsResponseMaximizer U a p q v) : (canonicalMaximizer ⋯ p q).toSolution.SameGradientAE v

Any response maximizer has the same gradient a.e. as the public canonical maximizer for the same loading. This is the deterministic Ch2 bridge needed when an upstream scalar-response selection is constructed by a Hilbert/Galerkin argument.

theorem HCPolySupport.Book.Ch02.canonicalMaximizer_sameGradientAE_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (p q : Vec d) : (Solution.ofAEEq h (canonicalMaximizer ⋯ p q).toSolution).SameGradientAE (canonicalMaximizer ⋯ p q).toSolution

Transporting the public canonical response maximizer across a coefficient a.e. equality gives a solution with the same gradient as the canonical maximizer for the transported coefficient.