First-order transport commutator identities for smooth Euclidean fields.

noncomputable def AVenhance.Infra.Section4.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.Section4.classicalTransport b u x = AVenhance.Infra.Classical.classicalTransport b u x

theorem AVenhance.Infra.Section4.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.Section4.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.Section4.ThetaCommutator.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.Section4.ThetaCommutator.classicalTransport_contDiff (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) (hb : ContDiff ℝ (↑⊤) b) (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ (↑⊤) (classicalTransport b u)

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

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

Equations

• AVenhance.Infra.Section4.classicalWordDerivative = AVenhance.Infra.Classical.classicalWordDerivative

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

def AVenhance.Infra.Section4.ThetaCommutator.thetaWordDirections (w : List (Fin 2)) : Fin w.length → Fin 2

Coordinate directions of a spatial derivative word indexed by its length.

Equations

• AVenhance.Infra.Section4.ThetaCommutator.thetaWordDirections w j = w.get j

theorem AVenhance.Infra.Section4.thetaWordDerivative_eq_iteratedFDeriv (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec 2) : classicalWordDerivative w f x = (iteratedFDeriv ℝ w.length f x) fun (j : Fin w.length) => Homogenization.basisVec (ThetaCommutator.thetaWordDirections w j)

The ordered-word convention agrees with iterated Fréchet differentiation on the corresponding ordered coordinate directions.

theorem AVenhance.Infra.Section4.thetaWordDerivative_eq_iteratedFDeriv_get (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec 2) : classicalWordDerivative w f x = (iteratedFDeriv ℝ w.length f x) fun (j : Fin w.length) => Homogenization.basisVec (w.get j)

The ordered derivative identification with the tuple written using List.get, for hypotheses quantified over all coordinate tuples.

theorem AVenhance.Infra.Section4.classicalWordDerivative_neg (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) : (classicalWordDerivative w fun (x : Homogenization.Vec 2) => -f x) = fun (x : Homogenization.Vec 2) => -classicalWordDerivative w f x

Negation passes through an ordered word of spatial derivatives.

theorem AVenhance.Infra.Section4.classicalWordDerivative_abs_le_of_iteratedFDeriv (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (B : ℝ) (hf : ContDiff ℝ (↑⊤) f) (hbound : ∀ (i : Fin w.length → Fin 2) (x : Homogenization.Vec 2), ‖(iteratedFDeriv ℝ w.length f x) fun (j : Fin w.length) => Homogenization.basisVec (i j)‖ ≤ B) (x : Homogenization.Vec 2) : |classicalWordDerivative w f x| ≤ B

Coordinate bounds for all order-n Fréchet derivatives immediately give the same bound for each ordered coordinate word.

theorem AVenhance.Infra.Section4.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.Section4.classicalWordDerivative_eq_of_perm (w v : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (h : w.Perm v) : classicalWordDerivative w f = classicalWordDerivative v f

Smooth ordered coordinate derivatives depend only on the multiset of directions. This lets a one-derivative Leibniz split be identified with one coordinate of the gradient of the complementary word.

theorem AVenhance.Infra.Section4.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.Section4.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.Section4.classicalContDiff_listSum (L : List (Homogenization.Vec 2 → ℝ)) (hL : ∀ f ∈ L, ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) L.sum

theorem AVenhance.Infra.Section4.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.Section4.classicalWordSplits : List (Fin 2) → List (List (Fin 2) × List (Fin 2))

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

Equations

• AVenhance.Infra.Section4.classicalWordSplits = AVenhance.Infra.Classical.classicalWordSplits

noncomputable def AVenhance.Infra.Section4.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.Section4.classicalWordProductTerm p f g = AVenhance.Infra.Classical.classicalWordProductTerm p f g

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

Leibniz expansion of an ordered word of coordinate derivatives.

Equations

• AVenhance.Infra.Section4.classicalWordProductExpansion w f g = AVenhance.Infra.Classical.classicalWordProductExpansion w f g

def AVenhance.Infra.Section4.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

• AVenhance.Infra.Section4.classicalWordCommutatorSplits = AVenhance.Infra.Classical.classicalWordCommutatorSplits

theorem AVenhance.Infra.Section4.ThetaCommutator.classicalPerm_move_head (i : Fin 2) (u v : List (Fin 2)) : (i :: u ++ v).Perm (u ++ i :: v)

theorem AVenhance.Infra.Section4.classicalWordSplits_perm_append (w : List (Fin 2)) {p : List (Fin 2) × List (Fin 2)} (hp : p ∈ classicalWordSplits w) : w.Perm (p.1 ++ p.2)

Every Leibniz split preserves the complete ordered derivative word up to permutation.

theorem AVenhance.Infra.Section4.classicalWordCommutatorSplits_perm_append (w : List (Fin 2)) {p : List (Fin 2) × List (Fin 2)} (hp : p ∈ classicalWordCommutatorSplits w) : w.Perm (p.1 ++ p.2)

The same shuffle invariant holds after the zero-derivative-on-drift term is removed from the transport commutator.

theorem AVenhance.Infra.Section4.classicalWordDerivative_sq_le_gradient_of_perm (w v : List (Fin 2)) (i : Fin 2) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec 2) (hperm : w.Perm (i :: v)) : classicalWordDerivative w f x ^ 2 ≤ Homogenization.vecNormSq (spaceGrad (classicalWordDerivative v f) x)

The order-n derivative in a split with one derivative on the stream potential is itself a coordinate of the gradient of the complementary order-n-1 derivative.

theorem AVenhance.Infra.Section4.classicalWordDerivative_sq_le_gradient_of_first_order_split (w : List (Fin 2)) (p : List (Fin 2) × List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec 2) (hp : p ∈ classicalWordCommutatorSplits w) (hq : p.1.length = 1) : classicalWordDerivative w f x ^ 2 ≤ Homogenization.vecNormSq (spaceGrad (classicalWordDerivative p.2 f) x)

Specialization of the coordinate estimate to a commutator split with one derivative on its first factor.

theorem AVenhance.Infra.Section4.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 full Leibniz split list contains choose n q occurrences with exactly q derivatives on its first factor, including multiplicities for repeated coordinate directions.

theorem AVenhance.Infra.Section4.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 transport commutator split list has the same binomial multiplicities, with the zero-derivative-on-drift split removed.

theorem AVenhance.Infra.Section4.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.Section4.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.Section4.classicalWordCommutatorSplits_left_ne_nil (w : List (Fin 2)) {p : List (Fin 2) × List (Fin 2)} (hp : p ∈ classicalWordCommutatorSplits w) : p.1 ≠ []

theorem AVenhance.Infra.Section4.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.Section4.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

• AVenhance.Infra.Section4.classicalWordCommutatorExpansion w f g = AVenhance.Infra.Classical.classicalWordCommutatorExpansion w f g

theorem AVenhance.Infra.Section4.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.Section4.ThetaCommutator.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.Section4.ThetaCommutator.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.Section4.ThetaCommutator.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.Section4.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.Section4.ThetaCommutator.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.Section4.ThetaCommutator.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.Section4.ThetaCommutator.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.Section4.ThetaCommutator.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.Section4.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.Section4.ThetaCommutator.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.Section4.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.Section4.ThetaCommutator.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.Section4.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.Section4.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.Section4.ThetaCommutator.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.Section4.ThetaCommutator.classicalList_abs_sum_le (L : List ℝ) : |L.sum| ≤ (List.map (fun (a : ℝ) => |a|) L).sum

theorem AVenhance.Infra.Section4.ThetaCommutator.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.Section4.ThetaCommutator.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.Section4.ThetaCommutator.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.Section4.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.Section4.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.Section4.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.Section4.ThetaCommutator.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