A local Fréchet derivative rule for a matrix-vector flux.

theorem AVenhance.Infra.Section5.hasFDerivAt_matrix_mulVec {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {V : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} {LA : Fin 2 → Fin 2 → Homogenization.Vec 2 →L[ℝ] ℝ} {LV : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hA : ∀ (i j : Fin 2), HasFDerivAt (fun (y : Homogenization.Vec 2) => A y i j) (LA i j) x) (hV : HasFDerivAt V LV x) : HasFDerivAt (fun (y : Homogenization.Vec 2) => (A y).mulVec (V y)) (ContinuousLinearMap.pi fun (i : Fin 2) => ∑ j : Fin 2, (V x j • LA i j + A x i j • ContinuousLinearMap.proj j ∘SL LV)) x

Entrywise matrix derivatives and a vector derivative give the Fréchet derivative of their pointwise matrix-vector product.