Transport Characteristic Jets

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.FaaDiBruno.list_ofFn_map {α : Type u_1} {β : Type u_2} {n : ℕ} (I : Fin n → α) (f : α → β) : (List.ofFn fun (j : Fin n) => f (I j)) = List.map f (List.ofFn I)

theorem AVenhance.FaaDiBruno.directionalJet_coordinateList_eq_orderedPartial (J : List (Fin 2)) {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec 2 → F) (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec 2) : directionalJet (List.map (coordinateVector 2) J) f x = orderedPartial J.length f x fun (j : Fin J.length) => J.get j

A list of coordinate directions is one of the ordered partials used in the paper's seminorm.

theorem AVenhance.FaaDiBruno.directionalJet_coordinateList_norm_le (J : List (Fin 2)) (f : Homogenization.Vec 2 → Homogenization.Vec 2) (hf : ContDiff ℝ (↑⊤) f) {C R : ℝ} (hR : 0 < R) (hC : 0 ≤ C) (hs : snorm f J.length R ≤ ENNReal.ofReal C) (x : Homogenization.Vec 2) : ‖directionalJet (List.map (coordinateVector 2) J) f x‖ ≤ C * ↑J.length.factorial * R ^ J.length / (↑J.length + 1) ^ 2

theorem AVenhance.FaaDiBruno.jointSpatialCoordinateComponentJet_eq_slice (J : List (Fin 2)) (b : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hb : ContDiff ℝ (↑⊤) b) (t : ℝ) (x : Homogenization.Vec 2) (i : Fin 2) : directionalJet (jointSpatialDirections (List.map (coordinateVector 2) J)) (fun (q : ℝ × Homogenization.Vec 2) => b q i) (t, x) = directionalJet (List.map (coordinateVector 2) J) (fun (y : Homogenization.Vec 2) => b (t, y)) x i

theorem AVenhance.FaaDiBruno.jointSpatialGradientJet_eq_slice (J : List (Fin 2)) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) F) (t : ℝ) (x : Homogenization.Vec 2) (i : Fin 2) : directionalJet (jointSpatialDirections (List.map (coordinateVector 2) J)) (fun (q : ℝ × Homogenization.Vec 2) => (fderiv ℝ F q) (0, coordinateVector 2 i)) (t, x) = directionalJet (List.map (coordinateVector 2) J ++ [coordinateVector 2 i]) (fun (y : Homogenization.Vec 2) => F (t, y)) x

theorem AVenhance.FaaDiBruno.TransportCharacteristicJets.list_sum_norm_le_of_forall {α : Type u_1} (L : List α) (f : α → Homogenization.Vec 2) (g : α → ℝ) (hfg : ∀ a ∈ L, ‖f a‖ ≤ g a) : ‖(List.map f L).sum‖ ≤ (List.map g L).sum

theorem AVenhance.FaaDiBruno.TransportCharacteristicJets.list_sum_add_const {α : Type u_1} (L : List α) (g : α → ℝ) (c : ℝ) : (List.map (fun (a : α) => c + g a) L).sum = ↑L.length * c + (List.map g L).sum

theorem AVenhance.FaaDiBruno.TransportCharacteristicJets.list_sum_le_of_forall {α : Type u_1} (L : List α) (f g : α → ℝ) (hfg : ∀ a ∈ L, f a ≤ g a) : (List.map f L).sum ≤ (List.map g L).sum

theorem AVenhance.FaaDiBruno.TransportCharacteristicJets.list_sum_map_add {α : Type u_1} (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.FaaDiBruno.TransportCharacteristicJets.list_sum_if_count {α : Type u_1} (L : List α) (p : α → Prop) [DecidablePred p] (c : ℝ) : (List.map (fun (a : α) => if p a then c else 0) L).sum = ↑(List.countP (fun (a : α) => decide (p a)) L) * c

theorem AVenhance.FaaDiBruno.TransportCharacteristicJets.orderedPartial_list_get_bound {n : ℕ} (K : List (Fin 2)) (hK : K.length = n) (f : Homogenization.Vec 2 → Homogenization.Vec 2) (x : Homogenization.Vec 2) {U : ℝ} (hU : ∀ (I : Fin n → Fin 2), ‖orderedPartial n f x I‖ ≤ U) : ‖orderedPartial K.length f x fun (j : Fin K.length) => K.get j‖ ≤ U

theorem AVenhance.FaaDiBruno.TransportCharacteristicJets.contDiff_slice_joint (f : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hf : ContDiff ℝ (↑⊤) (Function.uncurry f)) (t : ℝ) : ContDiff ℝ (↑⊤) (f t)

theorem AVenhance.FaaDiBruno.transportSourceJet_coordinate_norm_le_local {n : ℕ} (I : Fin n → Fin 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)) {C_f C_g R U T : ℝ} (RY : ℝ → ℝ) (hR : 0 < R) (hRY : ∀ (t : ℝ), 0 < RY t) (hCf : 0 ≤ C_f) (hCg : 0 ≤ C_g) (A : ℝ → ℕ → ℝ) (hA : ∀ (t : ℝ) (k : ℕ), 0 ≤ A t k) (hB : ∀ (t : ℝ) (m : ℕ), 1 ≤ m → m ≤ n → snorm (b t) m R ≤ ENNReal.ofReal C_f) (hG : ∀ (t : ℝ), snorm (g t) n R ≤ ENNReal.ofReal C_g) (hYbound : ∀ (t : ℝ), |t| ≤ T → ∀ (k : ℕ), 1 ≤ k → k < n → snorm (Y t) k (RY t) ≤ ENNReal.ofReal (A t k)) (t : ℝ) (ht : |t| ≤ T) (x : Homogenization.Vec 2) (hUjet : ∀ (J : Fin n → Fin 2), ‖orderedPartial n (Y t) x J‖ ≤ U) : ‖transportSourceJet (List.ofFn fun (j : Fin n) => coordinateVector 2 (I j)) b g Y (t, x)‖ ≤ C_g * ↑n.factorial * R ^ n / (↑n + 1) ^ 2 + 2 * (↑n * (C_f * R / 4 * U) + (List.map (fun (p : List (Fin 2) × List (Fin 2)) => if 2 ≤ p.1.length then C_f * ↑p.1.length.factorial * R ^ p.1.length / (↑p.1.length + 1) ^ 2 * (A t (p.2.length + 1) * ↑(p.2.length + 1).factorial * RY t ^ (p.2.length + 1) / (↑p.2.length + 2) ^ 2) else 0) (directionalSplitsNonempty (List.ofFn I))).sum)

A pointwise source estimate with the current order-n jet left as a linear term. This is the a-priori finiteness estimate used before the sharp corrected absorption.

theorem AVenhance.FaaDiBruno.transportSpatialJet_coordinate_eq_orderedPartial {n : ℕ} (I : Fin n → Fin 2) (Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hY : ContDiff ℝ (↑⊤) (Function.uncurry Y)) (t : ℝ) (x : Homogenization.Vec 2) : transportSpatialJet (List.ofFn fun (j : Fin n) => coordinateVector 2 (I j)) (Function.uncurry Y) (t, x) = orderedPartial n (Y t) x I

The joint spatial jet indexed by a coordinate tuple is the paper's ordered coordinate partial of the time slice.

theorem AVenhance.FaaDiBruno.transportSpatialJet_initial_zero_of_nonempty (I : List (Homogenization.Vec 2)) (hI : I ≠ []) {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (x : Homogenization.Vec 2) : transportSpatialJet I (Function.uncurry Y) (0, x) = 0

theorem AVenhance.FaaDiBruno.transportSolution_spatialJet_intervalIntegral (I : List (Homogenization.Vec 2)) (hI : I ≠ []) {b g Y : ℝ → Homogenization.Vec 2 → 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) (t : ℝ) : transportSpatialJet I (Function.uncurry Y) (t, X t x 0) = ∫ (r : ℝ) in 0..t, transportSourceJet I b g Y (r, X r x 0)

Every nonempty spatial jet of a zero-initial-data transport solution is the integral of its recursively differentiated source along a characteristic.