Transport Expansion

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.FaaDiBruno.transportSpatialJet_contDiff (I : List (Homogenization.Vec 2)) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (transportSpatialJet I F)

All finite spatial jets of a smooth joint field remain jointly smooth.

theorem AVenhance.FaaDiBruno.jointSpatialDirectionalDerivative_eq_slice (F : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) (Function.uncurry F)) (t : ℝ) (x v : Homogenization.Vec 2) : (fderiv ℝ (Function.uncurry F) (t, x)) (0, v) = (fderiv ℝ (F t) x) v

Evaluating a joint space derivative in a spatial direction is the ordinary derivative of the corresponding time slice.

theorem AVenhance.FaaDiBruno.transportSpatialJet_eq_directionalJet_slice (I : List (Homogenization.Vec 2)) (F : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) (Function.uncurry F)) (t : ℝ) : (fun (x : Homogenization.Vec 2) => transportSpatialJet I (Function.uncurry F) (t, x)) = directionalJet I (F t)

The recursively defined joint transport jet agrees with the ordinary ordered derivative of the fixed-time slice.

theorem AVenhance.FaaDiBruno.TransportExpansion.directionalJet_clm_apply {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] (I : List E) (c : E → E →L[ℝ] F) (hc : ContDiff ℝ (↑⊤) c) (v : E) : (directionalJet I fun (x : E) => (c x) v) = fun (x : E) => (directionalJet I c x) v

theorem AVenhance.FaaDiBruno.TransportExpansion.iteratedFDeriv_apply_directionalJet {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (F : Type) [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (hf : ContDiff ℝ (↑⊤) f) (x : E) (I : Fin n → E) : (iteratedFDeriv ℝ n f x) I = directionalJet (List.ofFn I) f x

theorem AVenhance.FaaDiBruno.TransportExpansion.directionalJet_comp_linear {E F G : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (I : List E) (f : F → G) (hf : ContDiff ℝ (↑⊤) f) (L : E →L[ℝ] F) (x : E) : directionalJet I (f ∘ ⇑L) x = directionalJet (List.map (⇑L) I) f (L x)

theorem AVenhance.FaaDiBruno.orderedPartial_eq_directionalJet {d n : ℕ} {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec d → F) (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec d) (I : Fin n → Fin d) : orderedPartial n f x I = directionalJet (List.ofFn fun (j : Fin n) => coordinateVector d (I j)) f x

The paper's ordered coordinate partial is the ordinary directional jet along the corresponding coordinate vectors on Vec d.