Transport Commutator

Support for the Armstrong–Vicol anomalous-diffusion formalization.

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

Allocations of an ordered direction list in which the left factor receives at least one direction.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.FaaDiBruno.directionalSplitsNonempty [] = []

theorem AVenhance.FaaDiBruno.directionalSplits_eq_nonempty_append_empty {E : Type u_1} (I : List E) : directionalSplits I = directionalSplitsNonempty I ++ [([], I)]

Every ordered Leibniz allocation is either nonempty on the left or is the single all-right allocation.

theorem AVenhance.FaaDiBruno.directionalSplits_length_sum {E : Type u_1} (I : List E) (p : List E × List E) (hp : p ∈ directionalSplits I) : p.1.length + p.2.length = I.length

theorem AVenhance.FaaDiBruno.directionalSplitsNonempty_length_sum {E : Type u_1} (I : List E) (p : List E × List E) (hp : p ∈ directionalSplitsNonempty I) : p.1.length + p.2.length = I.length

theorem AVenhance.FaaDiBruno.directionalSplitsNonempty_left_pos {E : Type u_1} (I : List E) (p : List E × List E) (hp : p ∈ directionalSplitsNonempty I) : 0 < p.1.length

theorem AVenhance.FaaDiBruno.directionalSplits_count_leftLength {E : Type u_1} (I : List E) (m : ℕ) : List.countP (fun (p : List E × List E) => decide (p.1.length = m)) (directionalSplits I) = I.length.choose m

theorem AVenhance.FaaDiBruno.directionalSplitsNonempty_count_leftLength_eq_one {E : Type u_1} (I : List E) : List.countP (fun (p : List E × List E) => decide (p.1.length = 1)) (directionalSplitsNonempty I) = I.length

theorem AVenhance.FaaDiBruno.directionalSplits_map {E : Type u_1} {F : Type u_2} (φ : E → F) (I : List E) : directionalSplits (List.map φ I) = List.map (fun (p : List E × List E) => (List.map φ p.1, List.map φ p.2)) (directionalSplits I)

theorem AVenhance.FaaDiBruno.directionalSplitsNonempty_map {E : Type u_1} {F : Type u_2} (φ : E → F) (I : List E) : directionalSplitsNonempty (List.map φ I) = List.map (fun (p : List E × List E) => (List.map φ p.1, List.map φ p.2)) (directionalSplitsNonempty I)

theorem AVenhance.FaaDiBruno.directionalSplits_weight_sum {E : Type u_1} (I : List E) (w : ℕ → ℝ) : (List.map (fun (p : List E × List E) => w p.1.length) (directionalSplits I)).sum = ∑ m ∈ Finset.range (I.length + 1), ↑(I.length.choose m) * w m

theorem AVenhance.FaaDiBruno.directionalSplitsNonempty_weight_sum {E : Type u_1} (I : List E) (w : ℕ → ℝ) : (List.map (fun (p : List E × List E) => w p.1.length) (directionalSplitsNonempty I)).sum = ∑ k ∈ Finset.range I.length, ↑(I.length.choose (k + 1)) * w (k + 1)

theorem AVenhance.FaaDiBruno.directionalJet_finset_sum {E : Type u_1} {ι : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (I : List E) (s : Finset ι) (f : ι → E → F) (hf : ∀ i ∈ s, ContDiff ℝ (↑⊤) (f i)) : (directionalJet I fun (x : E) => ∑ i ∈ s, f i x) = fun (x : E) => ∑ i ∈ s, directionalJet I (f i) x

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

theorem AVenhance.FaaDiBruno.directionalJet_add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (I : List E) (f g : E → F) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : (directionalJet I fun (x : E) => f x + g x) = fun (x : E) => directionalJet I f x + directionalJet I g x

theorem AVenhance.FaaDiBruno.directionalJet_sub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (I : List E) (f g : E → F) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : (directionalJet I fun (x : E) => f x - g x) = fun (x : E) => directionalJet I f x - directionalJet I g x

theorem AVenhance.FaaDiBruno.directionalJet_comp_clm {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (I : List E) (L : F →L[ℝ] G) (f : E → F) (hf : ContDiff ℝ (↑⊤) f) : (directionalJet I fun (x : E) => L (f x)) = fun (x : E) => L (directionalJet I f x)

noncomputable def AVenhance.FaaDiBruno.transportAdvection (b F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2

The spatial part of the transport derivative.

Equations

• AVenhance.FaaDiBruno.transportAdvection b F p = ∑ i : Fin 2, b p i • (fderiv ℝ F p) (0, AVenhance.FaaDiBruno.coordinateVector 2 i)

noncomputable def AVenhance.FaaDiBruno.jointTimeDerivative (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2

The time derivative of a joint field.

Equations

• AVenhance.FaaDiBruno.jointTimeDerivative F p = (fderiv ℝ F p) (1, 0)

def AVenhance.FaaDiBruno.jointSpatialDirections (I : List (Homogenization.Vec 2)) : List (ℝ × Homogenization.Vec 2)

The joint directions corresponding to an ordered list of spatial directions.

Equations

• AVenhance.FaaDiBruno.jointSpatialDirections I = List.map (fun (v : Homogenization.Vec 2) => (0, v)) I

theorem AVenhance.FaaDiBruno.jointSpatialDirectionalDerivative_eq_slice_general {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (G : ℝ × Homogenization.Vec 2 → F) (hG : ContDiff ℝ (↑⊤) G) (t : ℝ) (x v : Homogenization.Vec 2) : (fderiv ℝ G (t, x)) (0, v) = (fderiv ℝ (fun (y : Homogenization.Vec 2) => G (t, y)) x) v

theorem AVenhance.FaaDiBruno.jointSpatialDirectionalJet_eq_slice {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (I : List (Homogenization.Vec 2)) (G : ℝ × Homogenization.Vec 2 → F) (hG : ContDiff ℝ (↑⊤) G) (t : ℝ) (x : Homogenization.Vec 2) : directionalJet (jointSpatialDirections I) G (t, x) = directionalJet I (fun (y : Homogenization.Vec 2) => G (t, y)) x

theorem AVenhance.FaaDiBruno.transportAdvection_commutator_identity (I : List (Homogenization.Vec 2)) (b F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hb : ContDiff ℝ (↑⊤) b) (hF : ContDiff ℝ (↑⊤) F) : directionalJet (jointSpatialDirections I) (transportAdvection b F) - transportAdvection b (directionalJet (jointSpatialDirections I) F) = fun (p : ℝ × Homogenization.Vec 2) => ∑ i : Fin 2, (List.map (fun (split : List (ℝ × Homogenization.Vec 2) × List (ℝ × Homogenization.Vec 2)) => directionalJet split.1 (fun (q : ℝ × Homogenization.Vec 2) => b q i) p • directionalJet split.2 (fun (q : ℝ × Homogenization.Vec 2) => (fderiv ℝ F q) (0, coordinateVector 2 i)) p) (directionalSplitsNonempty (jointSpatialDirections I))).sum

theorem AVenhance.FaaDiBruno.transportSpatialJet_eq_jointDirectionalJet (I : List (Homogenization.Vec 2)) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) : transportSpatialJet I F = directionalJet (jointSpatialDirections I) F

theorem AVenhance.FaaDiBruno.jointTimeDerivative_contDiff (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (jointTimeDerivative F)

theorem AVenhance.FaaDiBruno.directionalJet_jointTime_commute (I : List (Homogenization.Vec 2)) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) F) : directionalJet (jointSpatialDirections I) (jointTimeDerivative F) = jointTimeDerivative (directionalJet (jointSpatialDirections I) F)

noncomputable def AVenhance.FaaDiBruno.jointTransportDerivative (b F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2

The space-time transport derivative of a joint field.

Equations

• AVenhance.FaaDiBruno.jointTransportDerivative b F p = (fderiv ℝ F p) (1, b p)

theorem AVenhance.FaaDiBruno.transportAdvection_contDiff (b F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hb : ContDiff ℝ (↑⊤) b) (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (transportAdvection b F)

theorem AVenhance.FaaDiBruno.jointTransportDerivative_eq_time_add_advection (b F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (p : ℝ × Homogenization.Vec 2) : jointTransportDerivative b F p = jointTimeDerivative F p + transportAdvection b F p

theorem AVenhance.FaaDiBruno.jointTransportCommutator (b F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hb : ContDiff ℝ (↑⊤) b) (hF : ContDiff ℝ (↑⊤) F) (t : ℝ) (x v : Homogenization.Vec 2) : (fderiv ℝ (fun (p : ℝ × Homogenization.Vec 2) => (fderiv ℝ F p) (0, v)) (t, x)) (1, b (t, x)) = (fderiv ℝ (jointTransportDerivative b F) (t, x)) (0, v) - (fderiv ℝ F (t, x)) (0, (fderiv ℝ b (t, x)) (0, v))

Differentiating the transport derivative in a fixed spatial direction produces the commutator with the spatial derivative of the drift.

theorem AVenhance.FaaDiBruno.TransportCommutator.jointDirectionalDerivative_contDiff {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] (G : ℝ × Homogenization.Vec 2 → F) (hG : ContDiff ℝ (↑⊤) G) (v : ℝ × Homogenization.Vec 2) : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => (fderiv ℝ G p) v

theorem AVenhance.FaaDiBruno.jointTransportDerivative_contDiff (b F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hb : ContDiff ℝ (↑⊤) b) (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (jointTransportDerivative b F)

Smoothness of the transport derivative of a smooth field.

theorem AVenhance.FaaDiBruno.transportSourceJet_contDiff (I : List (Homogenization.Vec 2)) (b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (hg : ContDiff ℝ (↑⊤) (Function.uncurry g)) (hY : ContDiff ℝ (↑⊤) (Function.uncurry Y)) : ContDiff ℝ (↑⊤) (transportSourceJet I b g Y)

Smoothness of the recursively generated source in the differentiated transport equation.

theorem AVenhance.FaaDiBruno.transportSourceJet_commutator_identity (I : List (Homogenization.Vec 2)) (b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (hg : ContDiff ℝ (↑⊤) (Function.uncurry g)) (hY : ContDiff ℝ (↑⊤) (Function.uncurry Y)) : transportSourceJet I b g Y = transportSpatialJet I (Function.uncurry g) - transportSpatialJet I (jointTransportDerivative (Function.uncurry b) (Function.uncurry Y)) + jointTransportDerivative (Function.uncurry b) (transportSpatialJet I (Function.uncurry Y))

The recursive commutator source equals the derivative-of-source minus the transport commutator, for every ordered spatial jet.

theorem AVenhance.FaaDiBruno.transportSourceJet_nonempty_identity (I : List (Homogenization.Vec 2)) (b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (hg : ContDiff ℝ (↑⊤) (Function.uncurry g)) (hY : ContDiff ℝ (↑⊤) (Function.uncurry Y)) : transportSourceJet I b g Y = transportSpatialJet I (Function.uncurry g) - fun (p : ℝ × Homogenization.Vec 2) => ∑ i : Fin 2, (List.map (fun (split : List (ℝ × Homogenization.Vec 2) × List (ℝ × Homogenization.Vec 2)) => directionalJet split.1 (fun (q : ℝ × Homogenization.Vec 2) => Function.uncurry b q i) p • directionalJet split.2 (fun (q : ℝ × Homogenization.Vec 2) => (fderiv ℝ (Function.uncurry Y) q) (0, coordinateVector 2 i)) p) (directionalSplitsNonempty (jointSpatialDirections I))).sum