Principal and lower-order terms in the ordered Leibniz expansion.

theorem AVenhance.Infra.Section4.iterateSpatialSplits_orders (w : List (Fin 2)) {p : List (Fin 2) × List (Fin 2)} (hp : p ∈ iterateSpatialSplits w) : p.1.length + p.2.length = w.length

The two derivative orders in every ordered split add to the original order.

theorem AVenhance.Infra.Section4.iterateSpatialSplits_nil_left (w : List (Fin 2)) : List.filter (fun (p : List (Fin 2) × List (Fin 2)) => p.1.isEmpty) (iterateSpatialSplits w) = [([], w)]

There is exactly one principal split: all derivatives fall on the scalar.

theorem AVenhance.Infra.Section4.iterate_split_list_sum {α : Type u_1} (P : List α) (f : α → ℝ) (q : α → Bool) : (List.map f P).sum = (List.map f (List.filter q P)).sum + (List.map f (List.filter (fun (p : α) => !q p) P)).sum

Splitting a list sum retains the principal and complementary terms exactly.

theorem AVenhance.Infra.Section4.iterateSpatialSplits_lower_order (w : List (Fin 2)) {p : List (Fin 2) × List (Fin 2)} (hp : p ∈ List.filter (fun (q : List (Fin 2) × List (Fin 2)) => !q.1.isEmpty) (iterateSpatialSplits w)) : p.2.length < w.length

Every complementary split has strictly fewer scalar derivatives.

noncomputable def AVenhance.Infra.Section4.iterateLowerWordFlux (A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (v : Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The strictly lower scalar-order portion of a differentiated matrix flux.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section4.iterateWordFlux_principal (A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (v : Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (x : Homogenization.Vec 2) : iterateWordFlux A v w x = (A x).mulVec (spaceGrad (iterateSpatialWord w v) x) + iterateLowerWordFlux A v w x

Separate the unique principal term from the full coefficient expansion.