Spatial product-rule lemmas for a finite cutoff ansatz.

theorem AVenhance.Infra.Section5.spaceGrad_finiteWeightedSum {ι : Type u_1} (S : Finset ι) (T H : Homogenization.Vec 2 → ℝ) (c : ι → ℝ) (P : ι → Homogenization.Vec 2 → ℝ) (x : Homogenization.Vec 2) {LT LH : Homogenization.Vec 2 →L[ℝ] ℝ} (LP : ι → Homogenization.Vec 2 →L[ℝ] ℝ) (hT : HasFDerivAt T LT x) (hH : HasFDerivAt H LH x) (hP : ∀ k ∈ S, HasFDerivAt (P k) (LP k) x) (i : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => T y + ∑ k ∈ S, c k * P k y + H y) x i = spaceGrad T x i + ∑ k ∈ S, c k * spaceGrad (P k) x i + spaceGrad H x i

Spatial gradient of a finite weighted sum, with the pointwise derivatives of the summands as the only regularity input.