Public statement.

noncomputable def AVenhance.Ingredients.flowGrad {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : Matrix (Fin 2) (Fin 2) ℝ

∇X_{m-1,l} ∘ X⁻¹_{m-1,l} (e.sm, e.chainrule.Tm1): the matrix whose (i,j) entry is ∂_i X^j_{m-1,l} evaluated at X⁻¹_{m-1,l}(t,x); row vectors for vector-valued functions and column vectors for gradients, exactly the convention of e.gradcorrmatrix (gradMatrix), so ∇(T∘X_l)∘X_l⁻¹ = (∇X_l∘X_l⁻¹) ∇T.

Equations

• I.flowGrad hΦ m l t x = AVenhance.gradMatrix (fun (y : Homogenization.Vec 2) => I.xFlow hΦ m l t y) (I.xFlowInv hΦ m l t x)