Iterates Divergence Add

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_vecDiv_add {A B : Homogenization.Vec 2 → Homogenization.Vec 2} (hA : ContDiff ℝ (↑⊤) A) (hB : ContDiff ℝ (↑⊤) B) (x : Homogenization.Vec 2) : vecDiv (fun (y : Homogenization.Vec 2) => A y + B y) x = vecDiv A x + vecDiv B x

Divergence is additive on the actual smooth vector carriers.

theorem AVenhance.Infra.Section4.iterate_constant_matrix_divergence (A : Matrix (Fin 2) (Fin 2) ℝ) {u : Homogenization.Vec 2 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (x : Homogenization.Vec 2) : vecDiv (fun (y : Homogenization.Vec 2) => A.mulVec (spaceGrad u y)) x = ∑ j : Fin 2, ∑ k : Fin 2, A j k * spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad u y k) x j

Divergence of a time-only matrix flux is its literal Hessian contraction.