Product-rule cancellation for a matrix transported along a flow.

theorem AVenhance.Infra.Section5.fderiv_scalar_eq_sum_spaceGrad {f : Homogenization.Vec 2 → ℝ} {x v : Homogenization.Vec 2} : (fderiv ℝ f x) v = ∑ p : Fin 2, v p * spaceGrad f x p

Expand a directional derivative in the coordinate basis.

theorem AVenhance.Infra.Section5.fderiv_vector_component_eq_sum_gradMatrix {F : Homogenization.Vec 2 → Homogenization.Vec 2} {x v : Homogenization.Vec 2} (hF : DifferentiableAt ℝ F x) (j : Fin 2) : (fderiv ℝ F x) v j = ∑ p : Fin 2, v p * gradMatrix F x p j

A component of the directional derivative of a vector field is the corresponding row-Jacobian contraction.

theorem AVenhance.Infra.Section5.hasDerivAt_matrixVec_mul_transport {A : ℝ → Matrix (Fin 2) (Fin 2) ℝ} {g : ℝ → Homogenization.Vec 2} {C : Matrix (Fin 2) (Fin 2) ℝ} {h : Homogenization.Vec 2} {t : ℝ} (i : Fin 2) (hA : ∀ (j : Fin 2), HasDerivAt (fun (r : ℝ) => A r i j) (∑ p : Fin 2, A t i p * C p j) t) (hg : ∀ (j : Fin 2), HasDerivAt (fun (r : ℝ) => g r j) (h j - ∑ p : Fin 2, C j p * g t p) t) : HasDerivAt (fun (r : ℝ) => (A r).mulVec (g r) i) ((A t).mulVec h i) t

Differentiating A g cancels the two velocity-gradient terms when A obeys the variational equation and g the material-gradient equation.