Characteristics

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.FaaDiBruno.transportSolution_hasDerivAt_alongFlow {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x : Homogenization.Vec 2) (s t : ℝ) : HasDerivAt (fun (r : ℝ) => Y r (X r x s)) (g t (X t x s)) t

Along a characterized flow trajectory, a classical transport solution has derivative equal to the source evaluated on that trajectory.

theorem AVenhance.FaaDiBruno.transportIteratedSpatialJet_hasDerivAt_alongFlow {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (I : List (Homogenization.Vec 2)) (hY : IsClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (hg : ContDiff ℝ (↑⊤) (Function.uncurry g)) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x : Homogenization.Vec 2) (s t : ℝ) : HasDerivAt (fun (r : ℝ) => transportSpatialJet I (Function.uncurry Y) (r, X r x s)) (transportSourceJet I b g Y (t, X t x s)) t

Along each flow characteristic, every finite ordered spatial derivative of a classical transport solution evolves by the recursively differentiated source above.

theorem AVenhance.FaaDiBruno.transportSolution_intervalIntegral_alongFlow {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (hg : ContDiff ℝ (↑⊤) (Function.uncurry g)) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x : Homogenization.Vec 2) (s t : ℝ) : Y t (X t x s) - Y s (X s x s) = ∫ (r : ℝ) in s..t, g r (X r x s)

The characteristic integral formula for a classical transport solution, valid on every oriented finite time interval.