GradientLinearity

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

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

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

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

Public a.e. additivity of response-maximizer gradients.

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

Public a.e. homogeneity of response-maximizer gradients.