Directional Product

Support for the Armstrong–Vicol anomalous-diffusion formalization.

def AVenhance.FaaDiBruno.directionalJet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (I : List E) (f : E → F) : E → F

Repeated differentiation in an ordered list of constant directions.

Equations

• AVenhance.FaaDiBruno.directionalJet [] f = f
• AVenhance.FaaDiBruno.directionalJet (v :: J) f = fun (x : E) => (fderiv ℝ (AVenhance.FaaDiBruno.directionalJet J f) x) v

def AVenhance.FaaDiBruno.directionalSplits {E : Type u_1} : List E → List (List E × List E)

Every allocation of an ordered direction list between two factors, retaining multiplicity when direction vectors repeat.

Equations

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

theorem AVenhance.FaaDiBruno.directionalJet_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (I : List E) (f : E → F) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (directionalJet I f)

theorem AVenhance.FaaDiBruno.directionalJet_append {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (I J : List E) (f : E → F) : directionalJet (I ++ J) f = directionalJet I (directionalJet J f)

Ordered directional jets concatenate without changing their order.

theorem AVenhance.FaaDiBruno.directionalJet_pair_swap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (hf : ContDiff ℝ (↑⊤) f) (v w : E) : directionalJet [v, w] f = directionalJet [w, v] f

Two adjacent spatial derivatives commute for a smooth field.

theorem AVenhance.FaaDiBruno.directionalJet_adjacent_swap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (P Q : List E) (f : E → F) (hf : ContDiff ℝ (↑⊤) f) (v w : E) : directionalJet (P ++ [v, w] ++ Q) f = directionalJet (P ++ [w, v] ++ Q) f

A swap of neighboring directions remains valid inside a longer ordered jet; all derivatives to its left are applied to the equality of the two second derivatives.

theorem AVenhance.FaaDiBruno.directionalJet_rotate_last {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (I : List E) (v : E) (f : E → F) (hf : ContDiff ℝ (↑⊤) f) : directionalJet (I ++ [v]) f = directionalJet (v :: I) f

Moving the final direction to the front of an ordered jet preserves its value for a smooth field.

theorem AVenhance.FaaDiBruno.DirectionalProduct.differentiableAt_list_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (l : List (E → F)) (x : E) (hl : ∀ f ∈ l, DifferentiableAt ℝ f x) : DifferentiableAt ℝ (fun (y : E) => (List.map (fun (f : E → F) => f y) l).sum) x

theorem AVenhance.FaaDiBruno.DirectionalProduct.list_sum_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (l : List (E →L[ℝ] F)) (v : E) : l.sum v = (List.map (fun (A : E →L[ℝ] F) => A v) l).sum

theorem AVenhance.FaaDiBruno.DirectionalProduct.fderiv_list_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (l : List (E → F)) (x : E) (hl : ∀ f ∈ l, DifferentiableAt ℝ f x) : fderiv ℝ (fun (y : E) => (List.map (fun (f : E → F) => f y) l).sum) x = (List.map (fun (f : E → F) => fderiv ℝ f x) l).sum

theorem AVenhance.FaaDiBruno.DirectionalProduct.contDiff_list_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (l : List (E → F)) (hl : ∀ f ∈ l, ContDiff ℝ (↑⊤) f) : ContDiff ℝ ↑⊤ fun (x : E) => (List.map (fun (f : E → F) => f x) l).sum

theorem AVenhance.FaaDiBruno.directionalJet_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (I : List E) (f g : E → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : (directionalJet I fun (x : E) => f x * g x) = fun (x : E) => (List.map (fun (p : List E × List E) => directionalJet p.1 f x * directionalJet p.2 g x) (directionalSplits I)).sum

theorem AVenhance.FaaDiBruno.directionalJet_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (I : List E) (a : E → ℝ) (f : E → F) (ha : ContDiff ℝ (↑⊤) a) (hf : ContDiff ℝ (↑⊤) f) : (directionalJet I fun (x : E) => a x • f x) = fun (x : E) => (List.map (fun (p : List E × List E) => directionalJet p.1 a x • directionalJet p.2 f x) (directionalSplits I)).sum

The ordered directional Leibniz expansion for a scalar multiple of a vector-valued field.