Transport Time Analyticity

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.FaaDiBruno.directionalSplits_append {E : Type u_1} (I J : List E) : directionalSplits (I ++ J) = List.flatMap (fun (p : List E × List E) => List.map (fun (q : List E × List E) => (p.1 ++ q.1, p.2 ++ q.2)) (directionalSplits J)) (directionalSplits I)

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

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

theorem AVenhance.FaaDiBruno.directionalSplits_replicate_parts {E : Type u_1} (a : E) {m : ℕ} (p : List E × List E) (hp : p ∈ directionalSplits (List.replicate m a)) : p.1 = List.replicate p.1.length a ∧ p.2 = List.replicate p.2.length a

theorem AVenhance.FaaDiBruno.TransportTimeAnalyticity.list_sum_flatMap {α : Type u_1} {β : Type u_2} [AddCommMonoid β] (L : List α) (f : α → List β) : (List.flatMap f L).sum = (List.map (fun (a : α) => (f a).sum) L).sum

theorem AVenhance.FaaDiBruno.directionalSplits_append_sum {E : Type u_1} {β : Type u_2} [AddCommMonoid β] (I J : List E) (f : List E × List E → β) : (List.map f (directionalSplits (I ++ J))).sum = (List.map (fun (p : List E × List E) => (List.map (fun (q : List E × List E) => f (p.1 ++ q.1, p.2 ++ q.2)) (directionalSplits J)).sum) (directionalSplits I)).sum

theorem AVenhance.FaaDiBruno.TransportTimeAnalyticity.nat_descFactorial_le_of_length_le {n k l : ℕ} (hkl : k ≤ l) (hl : l ≤ n) : n.descFactorial k ≤ n.descFactorial l

theorem AVenhance.FaaDiBruno.transportTime_factorialRatio_le {m n j k : ℕ} (hj : j ≤ m) (hk : k ≤ n) : ↑(k + j + 1).factorial / ↑k.factorial ≤ ↑(n + m + 1).factorial / ↑n.factorial

The factorial quotient in the two-parameter time/spatial induction is monotone in both derivative counts.

def AVenhance.FaaDiBruno.iteratedJointTimeDerivative : ℕ → (ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) → ℝ × Homogenization.Vec 2 → Homogenization.Vec 2

Repeated time derivatives of a joint field.

Equations

• AVenhance.FaaDiBruno.iteratedJointTimeDerivative 0 x✝ = x✝
• AVenhance.FaaDiBruno.iteratedJointTimeDerivative n.succ x✝ = AVenhance.FaaDiBruno.jointTimeDerivative (AVenhance.FaaDiBruno.iteratedJointTimeDerivative n x✝)

noncomputable def AVenhance.FaaDiBruno.transportTimeDerivative (m : ℕ) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2

The m-th time derivative of a joint field, as a time-dependent spatial field.

Equations

• AVenhance.FaaDiBruno.transportTimeDerivative m F = Function.curry (AVenhance.FaaDiBruno.iteratedJointTimeDerivative m F)

theorem AVenhance.FaaDiBruno.iteratedJointTimeDerivative_smooth (m : ℕ) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (iteratedJointTimeDerivative m F)

theorem AVenhance.FaaDiBruno.transportTimeDerivative_joint_smooth (m : ℕ) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (Function.uncurry (transportTimeDerivative m F))

theorem AVenhance.FaaDiBruno.directionalJet_spatial_commute_iteratedTime (I : List (Homogenization.Vec 2)) (m : ℕ) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) F) : directionalJet (jointSpatialDirections I) (iteratedJointTimeDerivative m F) = iteratedJointTimeDerivative m (directionalJet (jointSpatialDirections I) F)

theorem AVenhance.FaaDiBruno.orderedPartial_timeDerivative_eq_jointJet {m n : ℕ} (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) F) (t : ℝ) (x : Homogenization.Vec 2) (I : Fin n → Fin 2) : orderedPartial n (transportTimeDerivative m F t) x I = iteratedJointTimeDerivative m (directionalJet (jointSpatialDirections (List.ofFn fun (j : Fin n) => coordinateVector 2 (I j))) F) (t, x)

A mixed coordinate partial of a time derivative is the joint directional jet with the spatial directions followed by the time directions.

def AVenhance.FaaDiBruno.transportTimeDirections (m : ℕ) : List (ℝ × Homogenization.Vec 2)

Repeated pure time directions for an iterated joint derivative.

Equations

• AVenhance.FaaDiBruno.transportTimeDirections m = List.replicate m (1, 0)

def AVenhance.FaaDiBruno.jointCoordinateDirection (i : Fin 2) : ℝ × Homogenization.Vec 2

Embed one spatial coordinate direction into joint time-space.

Equations

• AVenhance.FaaDiBruno.jointCoordinateDirection i = (0, AVenhance.FaaDiBruno.coordinateVector 2 i)

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

Joint spatial directions associated with a list of coordinate indices.

Equations

• AVenhance.FaaDiBruno.transportCoordinateDirections I = AVenhance.FaaDiBruno.jointSpatialDirections (List.map (AVenhance.FaaDiBruno.coordinateVector 2) I)

theorem AVenhance.FaaDiBruno.transportCoordinateDirections_eq_map (I : List (Fin 2)) : transportCoordinateDirections I = List.map jointCoordinateDirection I

theorem AVenhance.FaaDiBruno.directionalSplits_coordinate_preimage {I : List (Fin 2)} {p : List (ℝ × Homogenization.Vec 2) × List (ℝ × Homogenization.Vec 2)} (hp : p ∈ directionalSplits (transportCoordinateDirections I)) : ∃ q ∈ directionalSplits I, p = (List.map jointCoordinateDirection q.1, List.map jointCoordinateDirection q.2)

theorem AVenhance.FaaDiBruno.directionalJet_component_norm_le (J : List (ℝ × Homogenization.Vec 2)) (B : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hB : ContDiff ℝ (↑⊤) B) (i : Fin 2) (p : ℝ × Homogenization.Vec 2) : ‖directionalJet J (fun (q : ℝ × Homogenization.Vec 2) => B q i) p‖ ≤ ‖directionalJet J B p‖

theorem AVenhance.FaaDiBruno.directionalJet_transportAdvection_full_splitSum (J : List (ℝ × Homogenization.Vec 2)) (B F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hB : ContDiff ℝ (↑⊤) B) (hF : ContDiff ℝ (↑⊤) F) : directionalJet J (transportAdvection B 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) (directionalSplits J)).sum

theorem AVenhance.FaaDiBruno.transportTimeMixedEquation (m : ℕ) (I : List (Fin 2)) {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (hg : ContDiff ℝ (↑⊤) (Function.uncurry g)) : directionalJet (transportTimeDirections m ++ transportCoordinateDirections I) (jointTimeDerivative (Function.uncurry Y)) = directionalJet (transportTimeDirections m ++ transportCoordinateDirections 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) (directionalSplits (transportTimeDirections m ++ transportCoordinateDirections I))).sum

theorem AVenhance.FaaDiBruno.directionalJet_timeDirections (m : ℕ) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) : directionalJet (transportTimeDirections m) F = iteratedJointTimeDerivative m F

theorem AVenhance.FaaDiBruno.directionalJet_mixedCoordinates_eq_iteratedTime_spatial (m : ℕ) (I : List (Fin 2)) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) : directionalJet (transportTimeDirections m ++ transportCoordinateDirections I) F = iteratedJointTimeDerivative m (directionalJet (transportCoordinateDirections I) F)

theorem AVenhance.FaaDiBruno.directionalJet_mixedCoordinates_eq_spatial_iteratedTime (m : ℕ) (I : List (Fin 2)) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) F) : directionalJet (transportTimeDirections m ++ transportCoordinateDirections I) F = directionalJet (transportCoordinateDirections I) (iteratedJointTimeDerivative m F)

theorem AVenhance.FaaDiBruno.directionalJet_mixedSpatialDerivative_eq_append (m : ℕ) (L : List (Fin 2)) (i : Fin 2) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) F) (p : ℝ × Homogenization.Vec 2) : directionalJet (transportTimeDirections m ++ transportCoordinateDirections L) (fun (q : ℝ × Homogenization.Vec 2) => (fderiv ℝ F q) (0, coordinateVector 2 i)) p = directionalJet (transportTimeDirections m ++ transportCoordinateDirections (L ++ [i])) F p

A spatial derivative of a mixed time-space jet is represented by the coordinate list with that derivative appended.

theorem AVenhance.FaaDiBruno.orderedPartial_timeDerivative_eq_coordinateListJet (m : ℕ) {n : ℕ} (I : Fin n → Fin 2) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) F) (t : ℝ) (x : Homogenization.Vec 2) : orderedPartial n (transportTimeDerivative m F t) x I = directionalJet (transportTimeDirections m ++ transportCoordinateDirections (List.ofFn I)) F (t, x)

The ordered joint jet of a time derivative and any finite list of coordinate spatial directions is the corresponding paper partial.

theorem AVenhance.FaaDiBruno.coordinateList_timeJet_norm_le_of_snorm {m n : ℕ} (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) F) (t : ℝ) (L : List (Fin 2)) (hL : L.length = n) {C R : ℝ} (hR : 0 < R) (hC : 0 ≤ C) (hs : snorm (transportTimeDerivative m F t) n R ≤ ENNReal.ofReal C) (x : Homogenization.Vec 2) : ‖directionalJet (transportTimeDirections m ++ transportCoordinateDirections L) F (t, x)‖ ≤ C * ↑n.factorial * R ^ n / (↑n + 1) ^ 2

A mixed jet indexed by an arbitrary finite coordinate list obeys the pointwise derivative bound read directly from the spatial seminorm.

theorem AVenhance.FaaDiBruno.snorm_le_of_radius_le {d n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec d → F) {R S C : ℝ} (hR : 0 < R) (hS : 0 < S) (hRS : R ≤ S) (hC : 0 ≤ C) (hs : snorm f n R ≤ ENNReal.ofReal C) : snorm f n S ≤ ENNReal.ofReal C

The paper's derivative seminorm decreases when its radius increases.

theorem AVenhance.FaaDiBruno.transportTimeLowerProduct_pointwise_bound {m n : ℕ} (L : List (Fin 2)) (hL : L.length = n) {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (hY : IsClassicalTransportSolution b g Y) {C_f Q_f R A Q ρ : ℝ} (hR : 0 < R) (hρ : 0 < ρ) (hCf : 0 ≤ C_f) (hQf : 0 ≤ Q_f) (hQ : 0 ≤ Q) (hA : 0 ≤ A) {p : List (ℝ × Homogenization.Vec 2) × List (ℝ × Homogenization.Vec 2)} (hp : p ∈ directionalSplits (transportTimeDirections m)) {q : List (ℝ × Homogenization.Vec 2) × List (ℝ × Homogenization.Vec 2)} (hq : q ∈ directionalSplits (transportCoordinateDirections L)) (i : Fin 2) (t : ℝ) (x : Homogenization.Vec 2) (hB : snorm (transportTimeDerivative p.1.length (Function.uncurry b) t) q.1.length R ≤ ENNReal.ofReal (C_f * Q_f ^ p.1.length * ↑p.1.length.factorial)) (hYbound : snorm (transportTimeDerivative p.2.length (Function.uncurry Y) t) (q.2.length + 1) ρ ≤ ENNReal.ofReal (A * (↑(q.2.length + p.2.length + 1).factorial * ↑p.2.length.factorial / ↑(q.2.length + 1).factorial) * Q ^ p.2.length)) : ‖directionalJet (p.1 ++ q.1) (fun (z : ℝ × Homogenization.Vec 2) => Function.uncurry b z i) (t, x) • directionalJet (p.2 ++ q.2) (fun (z : ℝ × Homogenization.Vec 2) => (fderiv ℝ (Function.uncurry Y) z) (0, coordinateVector 2 i)) (t, x)‖ ≤ C_f * Q_f ^ p.1.length * ↑p.1.length.factorial * (↑q.1.length.factorial * R ^ q.1.length / (↑q.1.length + 1) ^ 2) * (A * (↑(q.2.length + p.2.length + 1).factorial * ↑p.2.length.factorial / ↑(q.2.length + 1).factorial) * Q ^ p.2.length) * (↑(q.2.length + 1).factorial * ρ ^ (q.2.length + 1) / (↑q.2.length + 2) ^ 2)

One labeled mixed Leibniz summand is bounded by the exact two-factor coordinate-seminorm product used in the 10698 resummation.

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

theorem AVenhance.FaaDiBruno.TransportTimeAnalyticity.list_map_norm_sum_le {α : Type u_1} (L : List α) (f : α → Homogenization.Vec 2) : ‖(List.map f L).sum‖ ≤ (List.map (fun (a : α) => ‖f a‖) L).sum

theorem AVenhance.FaaDiBruno.directionalSplit_product_sum_bound {E : Type u_1} (I J : List E) (F : Fin 2 → List E × List E → List E × List E → Homogenization.Vec 2) (w : ℕ → ℕ → ℝ) (hF : ∀ (i : Fin 2), ∀ p ∈ directionalSplits I, ∀ q ∈ directionalSplits J, ‖F i p q‖ ≤ w p.2.length q.2.length) : ‖∑ i : Fin 2, (List.map (fun (p : List E × List E) => (List.map (fun (q : List E × List E) => F i p q) (directionalSplits J)).sum) (directionalSplits I)).sum‖ ≤ 2 * ∑ a ∈ Finset.range (I.length + 1), ∑ b ∈ Finset.range (J.length + 1), ↑(I.length.choose a) * ↑(J.length.choose b) * w a b

Bound a sum of mixed transport Leibniz terms by its length-only majorant. The two labeled split lists retain the binomial multiplicities exactly.

theorem AVenhance.FaaDiBruno.transportTimeAnalytic_scalar_budget {m n : ℕ} {C_f C_g R ρ Q Q_g : ℝ} (hCf : 0 < C_f) (hCg : 0 ≤ C_g) (hR : 0 < R) (hRρ : R ≤ ρ) (hρ : ρ ≤ 2 * R) (hQg0 : 0 ≤ Q_g) (hQg : Q_g ≤ Q) (hQ₁ : C_f * R ≤ Q) (hQ₂ : 16 * 2 * C_f * R ≤ Q) : C_g * Q_g ^ m * ↑m.factorial / (↑(m + 1).factorial * Q ^ (m + 1)) + 2 * C_f * (2 * C_g / (C_f * R)) * ρ / Q * ∑ j ∈ Finset.range (m + 1), ∑ k ∈ Finset.range (n + 1), (↑n + 1) ^ 2 / (↑(n - k + 1) ^ 2 * (↑k + 2) ^ 2 * (↑m + 1)) * (↑(k + j + 1).factorial / ↑k.factorial) ≤ 2 * C_g / (C_f * R) * (↑(n + m + 1).factorial / ↑n.factorial)

Scalar closure for one step of the 10698 time-derivative induction. The Q budget leaves half of the target for the source and half for the exact two-parameter convolution.