Target-time differentiation of the pulled gradient along its characteristic.

theorem AVenhance.Infra.Section5.gradMatrix_entry_eq_fderiv {X : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} (hX : DifferentiableAt ℝ X x) (i j : Fin 2) : gradMatrix X x i j = (fderiv ℝ X x) (Homogenization.basisVec i) j

An entry of the row-Jacobian convention is the corresponding Fréchet derivative evaluated on the coordinate vector.

theorem AVenhance.Infra.Section5.PulledGradientTransport.flow_jacobian_target_deriv_component {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s t : ℝ) (y : Homogenization.Vec 2) (i j : Fin 2) : HasDerivAt (fun (r : ℝ) => gradMatrix (fun (z : Homogenization.Vec 2) => X r z s) y i j) ((Flow.jointSpatialFDeriv b t (X t y s)) ((fderiv ℝ (fun (z : Homogenization.Vec 2) => X t z s) y) (Homogenization.basisVec i)) j) t

theorem AVenhance.Infra.Section5.flowGrad_material_deriv_component {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (y : Homogenization.Vec 2) (i j : Fin 2) : HasDerivAt (fun (r : ℝ) => I.flowGrad hΦ m l r (I.xFlow hΦ m l r y) i j) ((Flow.jointSpatialFDeriv (streamVel (Φ (m - 1))) t (I.xFlow hΦ m l t y)) ((fderiv ℝ (I.xFlow hΦ m l t) y) (Homogenization.basisVec i)) j) t

The pulled spatial Jacobian follows the linearized flow equation along the characteristic.