Exact ordered spatial Leibniz expansions for coefficient-gradient products.

def AVenhance.Infra.Section4.iterateSpatialSplits : List (Fin 2) → List (List (Fin 2) × List (Fin 2))

Each ordered derivative is assigned to exactly one of the two factors.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section4.iterateSpatialSplits [] = [([], [])]

theorem AVenhance.Infra.Section4.iterateSpatialSplits_length (w : List (Fin 2)) : (iterateSpatialSplits w).length = 2 ^ w.length

The full ordered expansion has exactly 2^n summands, before grouping by the order falling on a coefficient.

theorem AVenhance.Infra.Section4.IteratesWordLeibniz.iterate_word_list_differentiable (L : List (Homogenization.Vec 2 → ℝ)) (x : Homogenization.Vec 2) (h : ∀ f ∈ L, DifferentiableAt ℝ f x) : DifferentiableAt ℝ L.sum x

theorem AVenhance.Infra.Section4.IteratesWordLeibniz.iterate_word_list_gradient (L : List (Homogenization.Vec 2 → ℝ)) (x : Homogenization.Vec 2) (i : Fin 2) (h : ∀ f ∈ L, DifferentiableAt ℝ f x) : spaceGrad L.sum x i = (List.map (fun (f : Homogenization.Vec 2 → ℝ) => spaceGrad f x i) L).sum

theorem AVenhance.Infra.Section4.iterateSpatialWord_mul {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (w : List (Fin 2)) (x : Homogenization.Vec 2) : iterateSpatialWord w (f * g) x = (List.map (fun (p : List (Fin 2) × List (Fin 2)) => iterateSpatialWord p.1 f x * iterateSpatialWord p.2 g x) (iterateSpatialSplits w)).sum

Exact Leibniz rule at every spatial order. Repeated derivative letters are retained as separate ordered splits, producing the correct multiplicity.