Actual outer spatial derivatives of ordered material corrections.

def AVenhance.Infra.Section4.amnrSpatialAdvectionTerms : List (Fin 2) → List AmnrAdvectionTerm → List AmnrAdvectionTerm

Expand a list of advection terms under an ordered sequence of spatial derivatives.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section4.amnrSpatialAdvectionTerms [] x✝ = x✝

theorem AVenhance.Infra.Section4.amnrAdvectionDerivativeTerms_list_value {c : AmnrSpace → Homogenization.Vec 2} {v : Fin 2 → AmnrSpace → ℝ} {f : AmnrSpace → ℝ} (hc : ContDiff ℝ (↑⊤) c) (hv : ∀ (p : Fin 2), ContDiff ℝ (↑⊤) (v p)) (hf : ContDiff ℝ (↑⊤) f) (d : Option (Fin 2)) (T : List AmnrAdvectionTerm) (z : AmnrSpace) : amnrOp c d (List.map (amnrAdvectionTermValue c v f) T).sum z = (List.map (fun (t : AmnrAdvectionTerm) => amnrAdvectionTermValue c v f t z) (List.flatMap (fun (t : AmnrAdvectionTerm) => amnrAdvectionDerivativeTerms d t.factors t.scalarWord) T)).sum

theorem AVenhance.Infra.Section4.amnrSpatialAdvectionTerms_value {c : AmnrSpace → Homogenization.Vec 2} {v : Fin 2 → AmnrSpace → ℝ} {f : AmnrSpace → ℝ} (hc : ContDiff ℝ (↑⊤) c) (hv : ∀ (p : Fin 2), ContDiff ℝ (↑⊤) (v p)) (hf : ContDiff ℝ (↑⊤) f) (α : List (Fin 2)) (T : List AmnrAdvectionTerm) : amnrWord c (List.map some α) (List.map (amnrAdvectionTermValue c v f) T).sum = (List.map (amnrAdvectionTermValue c v f) (amnrSpatialAdvectionTerms α T)).sum

Every spatial word differentiates the actual finite correction sum into its explicit Leibniz list, preserving the order of all derivatives.

theorem AVenhance.Infra.Section4.amnrSpatialAdvectionTerms_counts (α : List (Fin 2)) (T : List AmnrAdvectionTerm) (t : AmnrAdvectionTerm) (ht : t ∈ amnrSpatialAdvectionTerms α T) : ∃ a ∈ T, t.factors.length = a.factors.length ∧ amnrTermMaterialCount t = amnrTermMaterialCount a ∧ amnrTermSpatialCount t = amnrTermSpatialCount a + α.length ∧ amnrSpatialCount a.scalarWord ≤ amnrSpatialCount t.scalarWord

Outer spatial differentiation changes only the total spatial count.

theorem AVenhance.Infra.Section4.amnrSpatialMaterialErrorTerms_counts (α : List (Fin 2)) (n : ℕ) (t : AmnrAdvectionTerm) (ht : t ∈ amnrSpatialAdvectionTerms α (amnrMaterialErrorTerms n)) : 1 ≤ t.factors.length ∧ 1 ≤ amnrSpatialCount t.scalarWord ∧ amnrTermSpatialCount t = t.factors.length + α.length ∧ amnrTermMaterialCount t + t.factors.length = n

Exact count identities after every outer spatial word and material level.