First-order transport commutator identities for smooth Euclidean fields.

noncomputable def AVenhance.Infra.Classical.classicalTransport (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) (x : Homogenization.Vec 2) : ℝ

The scalar transport term associated with a vector field and a scalar function.

Equations

• AVenhance.Infra.Classical.classicalTransport b u x = Homogenization.vecDot (b x) (AVenhance.spaceGrad u x)

theorem AVenhance.Infra.Classical.classicalProduct_firstDerivative (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => f y * g y) x i = f x * spaceGrad g x i + spaceGrad f x i * g x

Coordinate derivative of a product of two smooth scalar functions.

theorem AVenhance.Infra.Classical.classicalSpaceGrad_sub (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => f y - g y) x i = spaceGrad f x i - spaceGrad g x i

Coordinate derivative commutes with subtraction for smooth scalar functions.

theorem AVenhance.Infra.Classical.Commutator.classicalSpaceGrad_contDiff (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (i : Fin 2) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => spaceGrad f x i

theorem AVenhance.Infra.Classical.Commutator.classicalTransport_contDiff (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) (hb : ContDiff ℝ (↑⊤) b) (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ (↑⊤) (classicalTransport b u)

def AVenhance.Infra.Classical.classicalWordDerivative : List (Fin 2) → (Homogenization.Vec 2 → ℝ) → Homogenization.Vec 2 → ℝ

An ordered word of coordinate derivatives applied to a scalar function.

Equations

• AVenhance.Infra.Classical.classicalWordDerivative [] x✝ = x✝
• AVenhance.Infra.Classical.classicalWordDerivative (i :: w) x✝ = fun (x : Homogenization.Vec 2) => AVenhance.spaceGrad (AVenhance.Infra.Classical.classicalWordDerivative w x✝) x i

theorem AVenhance.Infra.Classical.classicalWordDerivative_contDiff (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (classicalWordDerivative w f)

theorem AVenhance.Infra.Classical.classicalSpaceGrad_commute (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (i j : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad f y j) x i = spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad f y i) x j

Smooth mixed coordinate derivatives commute.

theorem AVenhance.Infra.Classical.classicalWordDerivative_commute_gradient (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (j : Fin 2) : (classicalWordDerivative w fun (y : Homogenization.Vec 2) => spaceGrad f y j) = fun (x : Homogenization.Vec 2) => spaceGrad (classicalWordDerivative w f) x j

A coordinate derivative can be moved through an arbitrary ordered word of smooth coordinate derivatives.

theorem AVenhance.Infra.Classical.classicalSpaceGrad_add (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => f y + g y) x i = spaceGrad f x i + spaceGrad g x i

Coordinate derivative of a sum of smooth scalar functions.

theorem AVenhance.Infra.Classical.Commutator.classicalContDiff_listSum (L : List (Homogenization.Vec 2 → ℝ)) (hL : ∀ f ∈ L, ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) L.sum

theorem AVenhance.Infra.Classical.Commutator.classicalSpaceGrad_listSum (L : List (Homogenization.Vec 2 → ℝ)) (hL : ∀ f ∈ L, ContDiff ℝ (↑⊤) f) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad L.sum x i = (List.map (fun (f : Homogenization.Vec 2 → ℝ) => spaceGrad f x i) L).sum

def AVenhance.Infra.Classical.classicalWordSplits : List (Fin 2) → List (List (Fin 2) × List (Fin 2))

All ways of distributing an ordered derivative word between two factors.

Equations

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

noncomputable def AVenhance.Infra.Classical.classicalWordProductTerm (p : List (Fin 2) × List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) : Homogenization.Vec 2 → ℝ

The product term attached to one split of a derivative word.

Equations

• AVenhance.Infra.Classical.classicalWordProductTerm p f g x = AVenhance.Infra.Classical.classicalWordDerivative p.1 f x * AVenhance.Infra.Classical.classicalWordDerivative p.2 g x

noncomputable def AVenhance.Infra.Classical.classicalWordProductExpansion (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) : Homogenization.Vec 2 → ℝ

Leibniz expansion of an ordered word of coordinate derivatives.

Equations

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

def AVenhance.Infra.Classical.classicalWordCommutatorSplits : List (Fin 2) → List (List (Fin 2) × List (Fin 2))

The derivative splits with at least one derivative assigned to the first factor.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Classical.classicalWordCommutatorSplits [] = []

theorem AVenhance.Infra.Classical.classicalWordSplits_length (w : List (Fin 2)) {p : List (Fin 2) × List (Fin 2)} (hp : p ∈ classicalWordSplits w) : p.1.length + p.2.length = w.length

theorem AVenhance.Infra.Classical.classicalWordCommutatorSplits_length (w : List (Fin 2)) {p : List (Fin 2) × List (Fin 2)} (hp : p ∈ classicalWordCommutatorSplits w) : p.1.length + p.2.length = w.length

theorem AVenhance.Infra.Classical.classicalWordCommutatorSplits_left_ne_nil (w : List (Fin 2)) {p : List (Fin 2) × List (Fin 2)} (hp : p ∈ classicalWordCommutatorSplits w) : p.1 ≠ []

theorem AVenhance.Infra.Classical.classicalWordCommutatorSplits_right_length_lt (w : List (Fin 2)) {p : List (Fin 2) × List (Fin 2)} (hp : p ∈ classicalWordCommutatorSplits w) : p.2.length < w.length

noncomputable def AVenhance.Infra.Classical.classicalWordCommutatorExpansion (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) : Homogenization.Vec 2 → ℝ

The finite Leibniz sum over splits with a nonempty first derivative word.

Equations

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

theorem AVenhance.Infra.Classical.Commutator.classicalListSum_eval (L : List (Homogenization.Vec 2 → ℝ)) (x : Homogenization.Vec 2) : L.sum x = (List.map (fun (f : Homogenization.Vec 2 → ℝ) => f x) L).sum

theorem AVenhance.Infra.Classical.Commutator.classicalListSum_map_add {α : Type} (L : List α) (f g : α → ℝ) : (List.map (fun (a : α) => f a + g a) L).sum = (List.map f L).sum + (List.map g L).sum

theorem AVenhance.Infra.Classical.Commutator.classicalWordProductTerm_contDiff (p : List (Fin 2) × List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : ContDiff ℝ (↑⊤) (classicalWordProductTerm p f g)

theorem AVenhance.Infra.Classical.Commutator.classicalWordProductTerm_firstDerivative (p : List (Fin 2) × List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (classicalWordProductTerm p f g) x i = classicalWordProductTerm (i :: p.1, p.2) f g x + classicalWordProductTerm (p.1, i :: p.2) f g x

theorem AVenhance.Infra.Classical.Commutator.classicalWordCommutatorExpansion_firstDerivative (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (classicalWordCommutatorExpansion w f g) x i = (List.map (fun (p : List (Fin 2) × List (Fin 2)) => classicalWordProductTerm (i :: p.1, p.2) f g x) (classicalWordCommutatorSplits w)).sum + (List.map (fun (p : List (Fin 2) × List (Fin 2)) => classicalWordProductTerm (p.1, i :: p.2) f g x) (classicalWordCommutatorSplits w)).sum

theorem AVenhance.Infra.Classical.Commutator.classicalWordProductTerm_left_derivative (p : List (Fin 2) × List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (i : Fin 2) (x : Homogenization.Vec 2) : classicalWordProductTerm p (fun (y : Homogenization.Vec 2) => spaceGrad f y i) g x = classicalWordProductTerm (i :: p.1, p.2) f g x

theorem AVenhance.Infra.Classical.Commutator.classicalWordProductTerm_right_derivative (p : List (Fin 2) × List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 2) (x : Homogenization.Vec 2) : classicalWordProductTerm p f (fun (y : Homogenization.Vec 2) => spaceGrad g y i) x = classicalWordProductTerm (p.1, i :: p.2) f g x

theorem AVenhance.Infra.Classical.Commutator.classicalWordProductExpansion_left_derivative (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (i : Fin 2) (x : Homogenization.Vec 2) : classicalWordProductExpansion w (fun (y : Homogenization.Vec 2) => spaceGrad f y i) g x = (List.map (fun (p : List (Fin 2) × List (Fin 2)) => classicalWordProductTerm (i :: p.1, p.2) f g x) (classicalWordSplits w)).sum

theorem AVenhance.Infra.Classical.Commutator.classicalWordCommutatorExpansion_left_derivative (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (i : Fin 2) (x : Homogenization.Vec 2) : classicalWordCommutatorExpansion w (fun (y : Homogenization.Vec 2) => spaceGrad f y i) g x = (List.map (fun (p : List (Fin 2) × List (Fin 2)) => classicalWordProductTerm (i :: p.1, p.2) f g x) (classicalWordCommutatorSplits w)).sum

theorem AVenhance.Infra.Classical.Commutator.classicalWordCommutatorExpansion_right_derivative (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 2) (x : Homogenization.Vec 2) : classicalWordCommutatorExpansion w f (fun (y : Homogenization.Vec 2) => spaceGrad g y i) x = (List.map (fun (p : List (Fin 2) × List (Fin 2)) => classicalWordProductTerm (p.1, i :: p.2) f g x) (classicalWordCommutatorSplits w)).sum

theorem AVenhance.Infra.Classical.Commutator.classicalWordCommutatorExpansion_cons (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 2) (x : Homogenization.Vec 2) : classicalWordCommutatorExpansion (i :: w) f g x = classicalWordProductExpansion w (fun (y : Homogenization.Vec 2) => spaceGrad f y i) g x + classicalWordCommutatorExpansion w f (fun (y : Homogenization.Vec 2) => spaceGrad g y i) x

theorem AVenhance.Infra.Classical.Commutator.classicalWordCommutatorExpansion_contDiff (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : ContDiff ℝ (↑⊤) (classicalWordCommutatorExpansion w f g)

theorem AVenhance.Infra.Classical.Commutator.classicalWordProductExpansion_firstDerivative (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (classicalWordProductExpansion w f g) x i = classicalWordProductExpansion (i :: w) f g x

theorem AVenhance.Infra.Classical.classicalWordDerivative_mul (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : (classicalWordDerivative w fun (x : Homogenization.Vec 2) => f x * g x) = classicalWordProductExpansion w f g

An arbitrary ordered coordinate derivative of a product is the finite Leibniz sum over all ways to distribute its derivative word between the factors.

theorem AVenhance.Infra.Classical.classicalWordDerivative_mul_commutator (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : (classicalWordDerivative w fun (x : Homogenization.Vec 2) => f x * g x) = fun (x : Homogenization.Vec 2) => f x * classicalWordDerivative w g x + classicalWordCommutatorExpansion w f g x

The order-s transport commutator is precisely the Leibniz sum over splits that differentiate the drift at least once.

theorem AVenhance.Infra.Classical.Commutator.classicalWordDerivative_product_commutator_eq (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (x : Homogenization.Vec 2) : classicalWordProductExpansion w f g x - f x * classicalWordDerivative w g x = classicalWordCommutatorExpansion w f g x

theorem AVenhance.Infra.Classical.Commutator.classicalList_abs_sum_le (L : List ℝ) : |L.sum| ≤ (List.map (fun (a : ℝ) => |a|) L).sum

theorem AVenhance.Infra.Classical.Commutator.classicalWordCommutatorExpansion_abs_le (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (x : Homogenization.Vec 2) : |classicalWordCommutatorExpansion w f g x| ≤ (List.map (fun (p : List (Fin 2) × List (Fin 2)) => |classicalWordProductTerm p f g x|) (classicalWordCommutatorSplits w)).sum

theorem AVenhance.Infra.Classical.Commutator.classicalWordDerivative_finSum (w : List (Fin 2)) (f : Fin 2 → Homogenization.Vec 2 → ℝ) (hf : ∀ (j : Fin 2), ContDiff ℝ (↑⊤) (f j)) : (classicalWordDerivative w fun (x : Homogenization.Vec 2) => ∑ j : Fin 2, f j x) = fun (x : Homogenization.Vec 2) => ∑ j : Fin 2, classicalWordDerivative w (f j) x

theorem AVenhance.Infra.Classical.Commutator.classicalTransport_eq_finSum (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) : classicalTransport b u = fun (x : Homogenization.Vec 2) => ∑ j : Fin 2, b x j * spaceGrad u x j

theorem AVenhance.Infra.Classical.classicalWordDerivative_transport (w : List (Fin 2)) (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) (hb : ContDiff ℝ (↑⊤) b) (hu : ContDiff ℝ (↑⊤) u) : classicalWordDerivative w (classicalTransport b u) = fun (x : Homogenization.Vec 2) => ∑ j : Fin 2, classicalWordProductExpansion w (fun (y : Homogenization.Vec 2) => b y j) (fun (y : Homogenization.Vec 2) => spaceGrad u y j) x

Arbitrary ordered derivatives of the transport term are given by the finite Leibniz sum over the drift components and all derivative splits.

theorem AVenhance.Infra.Classical.classicalWordDerivative_transport_commutator (w : List (Fin 2)) (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) (hb : ContDiff ℝ (↑⊤) b) (hu : ContDiff ℝ (↑⊤) u) (x : Homogenization.Vec 2) : classicalWordDerivative w (classicalTransport b u) x - Homogenization.vecDot (b x) (spaceGrad (classicalWordDerivative w u) x) = ∑ j : Fin 2, (classicalWordProductExpansion w (fun (y : Homogenization.Vec 2) => b y j) (fun (y : Homogenization.Vec 2) => spaceGrad u y j) x - b x j * classicalWordDerivative w (fun (y : Homogenization.Vec 2) => spaceGrad u y j) x)

The arbitrary order transport commutator is the sum of exactly the Leibniz terms in which a derivative lands on the drift, written as the full product expansion with its principal term removed componentwise.

theorem AVenhance.Infra.Classical.classicalWordDerivative_transport_eq_commutatorExpansion (w : List (Fin 2)) (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) (hb : ContDiff ℝ (↑⊤) b) (hu : ContDiff ℝ (↑⊤) u) (x : Homogenization.Vec 2) : classicalWordDerivative w (classicalTransport b u) x - Homogenization.vecDot (b x) (spaceGrad (classicalWordDerivative w u) x) = ∑ j : Fin 2, classicalWordCommutatorExpansion w (fun (y : Homogenization.Vec 2) => b y j) (fun (y : Homogenization.Vec 2) => spaceGrad u y j) x

After cancelling the principal transport derivative, the order-s commutator is the finite sum of the Leibniz terms that differentiate a drift component.

theorem AVenhance.Infra.Classical.Commutator.classicalList_sum_mono {α : Type} (L : List α) (f g : α → ℝ) (h : ∀ a ∈ L, f a ≤ g a) : (List.map f L).sum ≤ (List.map g L).sum

theorem AVenhance.Infra.Classical.classicalTransport_firstCommutator (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) (hb : ContDiff ℝ (↑⊤) b) (hu : ContDiff ℝ (↑⊤) u) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (classicalTransport b u) x i - Homogenization.vecDot (b x) (spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad u y i) x) = ∑ j : Fin 2, spaceGrad (fun (y : Homogenization.Vec 2) => b y j) x i * spaceGrad u x j

The first derivative commutator between transport and a coordinate derivative is the product of the differentiated drift and the gradient of the scalar.

theorem AVenhance.Infra.Classical.classicalWordSplits_leftLength_count (w : List (Fin 2)) (q : ℕ) : (List.filter (fun (p : List (Fin 2) × List (Fin 2)) => decide (p.1.length = q)) (classicalWordSplits w)).length = w.length.choose q

The Leibniz split list has binomial multiplicities for the number of derivatives assigned to its first factor.

theorem AVenhance.Infra.Classical.classicalWordCommutatorSplits_leftLength_count (w : List (Fin 2)) (q : ℕ) : (List.filter (fun (p : List (Fin 2) × List (Fin 2)) => decide (p.1.length = q)) (classicalWordCommutatorSplits w)).length = if q = 0 then 0 else w.length.choose q

The commutator split list has the same binomial multiplicities, with the zero-derivative on the first factor removed.