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

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

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

Public theorem package for linearity of response-maximizer gradients.

The statement is made for arbitrary maximizers and uses a.e. gradient equality. This keeps it independent of the particular chosen representative returned by canonicalMaximizer. The canonical public theorem proving this package is responseGradientLinearityTheory in GradientLinearity.lean.

• add_gradient (p1 q1 p2 q2 : Vec d) (v12 v1 v2 : Solution U a) : IsResponseMaximizer U a (p1 + p2) (q1 + q2) v12 → IsResponseMaximizer U a p1 q1 v1 → IsResponseMaximizer U a p2 q2 v2 → v12.toH1.grad =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => v1.toH1.grad x + v2.toH1.grad x
• smul_gradient (c : ℝ) (p q : Vec d) (vc v : Solution U a) : IsResponseMaximizer U a (c • p) (c • q) vc → IsResponseMaximizer U a p q v → vc.toH1.grad =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => c • v.toH1.grad x

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

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

theorem HCPolySupport.Book.Ch02.gradient_add_of_response_maximizers {d : ℕ} {U : Domain d} {a : CoeffOn U} (hLinear : ResponseGradientLinearityTheory U a) {p1 q1 p2 q2 : Vec d} {v12 v1 v2 : Solution U a} (h12 : IsResponseMaximizer U a (p1 + p2) (q1 + q2) v12) (h1 : IsResponseMaximizer U a p1 q1 v1) (h2 : IsResponseMaximizer U a p2 q2 v2) : v12.toH1.grad =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => v1.toH1.grad x + v2.toH1.grad x

theorem HCPolySupport.Book.Ch02.gradient_smul_of_response_maximizers {d : ℕ} {U : Domain d} {a : CoeffOn U} (hLinear : ResponseGradientLinearityTheory U a) {c : ℝ} {p q : Vec d} {vc v : Solution U a} (hc : IsResponseMaximizer U a (c • p) (c • q) vc) (hv : IsResponseMaximizer U a p q v) : vc.toH1.grad =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => c • v.toH1.grad x

theorem HCPolySupport.Book.Ch02.canonicalMaximizer_add_gradientAE {d : ℕ} {U : Domain d} {a : CoeffOn U} (hTheory : ResponseExistenceTheory U a) (hLinear : ResponseGradientLinearityTheory U a) (p1 q1 p2 q2 : Vec d) : (canonicalMaximizer hTheory (p1 + p2) (q1 + q2)).toSolution.toH1.grad =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => (canonicalMaximizer hTheory p1 q1).toSolution.toH1.grad x + (canonicalMaximizer hTheory p2 q2).toSolution.toH1.grad x

theorem HCPolySupport.Book.Ch02.canonicalMaximizer_smul_gradientAE {d : ℕ} {U : Domain d} {a : CoeffOn U} (hTheory : ResponseExistenceTheory U a) (hLinear : ResponseGradientLinearityTheory U a) (c : ℝ) (p q : Vec d) : (canonicalMaximizer hTheory (c • p) (c • q)).toSolution.toH1.grad =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => c • (canonicalMaximizer hTheory p q).toSolution.toH1.grad x