Transport High Order

Support for the Armstrong–Vicol anomalous-diffusion formalization.

noncomputable def AVenhance.FaaDiBruno.orderedSpatialJetArray (n : ℕ) (f : Homogenization.Vec 2 → Homogenization.Vec 2) (x : Homogenization.Vec 2) : (Fin n → Fin 2) → Homogenization.Vec 2

The finite array of all coordinate partials of order n at one point.

Equations

• AVenhance.FaaDiBruno.orderedSpatialJetArray n f x I = AVenhance.FaaDiBruno.orderedPartial n f x I

noncomputable def AVenhance.FaaDiBruno.transportSpatialSourceArray (n : ℕ) (b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) : (Fin n → Fin 2) → Homogenization.Vec 2

The array of recursively differentiated transport sources for all coordinate partials of order n.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.FaaDiBruno.transportLowerAllocationWeight (n m : ℕ) (C_f C_g R ρ s : ℝ) : ℝ

The lower-allocation weight after inserting the induction bound 16 C_g s in the transport source estimate.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.FaaDiBruno.transportLowerAllocationSum {n : ℕ} (I : Fin n → Fin 2) (C_f C_g R ρ s : ℝ) : ℝ

The summed lower-allocation source weight, expressed on the ordered coordinate list.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.FaaDiBruno.transportLowerAllocationSum_eq_binomial {n : ℕ} (hn : 2 ≤ n) (I : Fin n → Fin 2) (C_f C_g R ρ s : ℝ) : transportLowerAllocationSum I C_f C_g R ρ s = ∑ k ∈ Finset.range (n - 1), ↑(n.choose k) * (C_f * ↑(n - k).factorial * R ^ (n - k) / (↑n - ↑k + 1) ^ 2 * (16 * C_g * s * ↑(k + 1).factorial * ρ ^ (k + 1) / (↑k + 2) ^ 2))

Regrouping the lower source allocations by their right-hand order gives the binomial sum in the transport proof.

noncomputable def AVenhance.FaaDiBruno.transportLowerAllocationMajorant (n : ℕ) (C_f C_g R ρmax T : ℝ) : ℝ

A time-independent majorant for the lower-allocation source at times s ≤ T and radii ρ ≤ ρmax.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.FaaDiBruno.transportLowerAllocationSum_le_majorant {n : ℕ} (hn : 2 ≤ n) (I : Fin n → Fin 2) {C_f C_g R ρ s T ρmax : ℝ} (hCf : 0 ≤ C_f) (hCg : 0 ≤ C_g) (hR : 0 ≤ R) (hT : 0 ≤ T) (hsT : s ≤ T) (hρ : 0 ≤ ρ) (hρmax : ρ ≤ ρmax) : transportLowerAllocationSum I C_f C_g R ρ s ≤ transportLowerAllocationMajorant n C_f C_g R ρmax T

def AVenhance.FaaDiBruno.transportShiftRadius (C_f R t : ℝ) : ℝ

The equal-radius transport scale on the forward time interval.

Equations

• AVenhance.FaaDiBruno.transportShiftRadius C_f R t = R + 8 * t * C_f * R ^ 2

theorem AVenhance.FaaDiBruno.transportShiftRadius_lower {C_f R t : ℝ} (ht : 0 ≤ t) (hCf : 0 ≤ C_f) : R ≤ transportShiftRadius C_f R t

theorem AVenhance.FaaDiBruno.transportShiftRadius_upper {C_f R t : ℝ} (hCf : 0 < C_f) (hR : 0 < R) (hT : t ≤ 1 / (8 * C_f * R)) : transportShiftRadius C_f R t ≤ 2 * R

theorem AVenhance.FaaDiBruno.transportLowerAllocationMajorant_nonneg {n : ℕ} {C_f C_g R ρ T : ℝ} (hCf : 0 ≤ C_f) (hCg : 0 ≤ C_g) (hR : 0 ≤ R) (hρ : 0 ≤ ρ) (hT : 0 ≤ T) : 0 ≤ transportLowerAllocationMajorant n C_f C_g R ρ T

theorem AVenhance.FaaDiBruno.transportField_lipschitz_of_snorm_one {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {C_f R : ℝ} (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (hCf : 0 ≤ C_f) (hR : 0 < R) (hB : ∀ (t : ℝ), snorm (b t) 1 R ≤ ENNReal.ofReal C_f) : ∃ (L : ℝ), 0 ≤ L ∧ ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖

theorem AVenhance.FaaDiBruno.transportSourceArray_norm_le_of_lower_bounds {n : ℕ} (hn : 2 ≤ n) {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (hg : ContDiff ℝ (↑⊤) (Function.uncurry g)) {C_f C_g R T : ℝ} (hCf : 0 < C_f) (hCg : 0 ≤ C_g) (hR : 0 < R) (hT : 0 ≤ T) (hTmax : T ≤ 1 / (8 * C_f * R)) (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) (hLower : ∀ (k : ℕ), 1 ≤ k → k < n → ∀ (t : ℝ), |t| ≤ T → snorm (Y t) k (transportShiftRadius C_f R |t|) ≤ ENNReal.ofReal (16 * C_g * |t|)) (t : ℝ) : |t| ≤ T → ∀ (x : Homogenization.Vec 2), ‖transportSpatialSourceArray n b g Y t x‖ ≤ ↑n * C_f * R / 2 * ‖orderedSpatialJetArray n (Y t) x‖ + (C_g * ↑n.factorial * R ^ n / (↑n + 1) ^ 2 + 2 * transportLowerAllocationMajorant n C_f C_g R (2 * R) T)

The differentiated transport source is bounded by a linear top-order jet term and a finite lower-order forcing, using the equal-radius induction hypothesis on [-T,T].

theorem AVenhance.FaaDiBruno.transportSourceJet_norm_le_sharp {n : ℕ} (hn : 2 ≤ n) (I : Fin n → 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)) {C_f C_g R T U : ℝ} (hCf : 0 < C_f) (hCg : 0 ≤ C_g) (hR : 0 < R) (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) (hLower : ∀ (k : ℕ), 1 ≤ k → k < n → ∀ (t : ℝ), |t| ≤ T → snorm (Y t) k (transportShiftRadius C_f R |t|) ≤ ENNReal.ofReal (16 * C_g * |t|)) (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 + ↑n * C_f * R / 2 * U + 2 * ∑ k ∈ Finset.range (n - 1), ↑(n.choose k) * (C_f * ↑(n - k).factorial * R ^ (n - k) / (↑n - ↑k + 1) ^ 2 * (16 * C_g * |t| * ↑(k + 1).factorial * transportShiftRadius C_f R |t| ^ (k + 1) / (↑k + 2) ^ 2))

The sharp differentiated source estimate in binomial order. This is the form whose time integral gives the corrected coefficient and the corrected shifted convolution.

def AVenhance.FaaDiBruno.transportJetRatioSet {n : ℕ} (Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (C_f R T : ℝ) : Set ℝ

The normalized coordinate-jet ratios used in the a-priori finiteness step and the sharp absorption.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.FaaDiBruno.transportJetRatioSet_bddAbove {n : ℕ} (Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) {C_f R T D : ℝ} (hCf : 0 ≤ C_f) (hR : 0 < R) (hD : 0 ≤ D) (hpoint : ∀ (t : ℝ), |t| ≤ T → ∀ (I : Fin n → Fin 2) (x : Homogenization.Vec 2), ‖orderedPartial n (Y t) x I‖ ≤ |t| * D) : BddAbove (transportJetRatioSet Y C_f R T)

theorem AVenhance.FaaDiBruno.orderedSpatialJetArray_hasDerivAt_alongFlow {n : ℕ} {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) (s t : ℝ) : HasDerivAt (fun (r : ℝ) => orderedSpatialJetArray n (Y r) (X r x s)) (transportSpatialSourceArray n b g Y t (X t x s)) t

All order-n coordinate partials evolve as one finite-dimensional ODE along a flow characteristic.

theorem AVenhance.FaaDiBruno.orderedSpatialJetArray_initial_zero {n : ℕ} (hn : 0 < n) {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (x : Homogenization.Vec 2) : orderedSpatialJetArray n (Y 0) x = 0

The initial value of every positive-order coordinate-jet array is zero.

theorem AVenhance.FaaDiBruno.orderedSpatialJet_norm_le_gronwall_forward {n : ℕ} (hn : 0 < n) {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) (hLip : ∃ (L : ℝ), ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖) {t L F : ℝ} (ht : 0 ≤ t) (hsource : ∀ r ∈ Set.Ico 0 t, ∀ (x : Homogenization.Vec 2), ‖transportSpatialSourceArray n b g Y r x‖ ≤ L * ‖orderedSpatialJetArray n (Y r) x‖ + F) (y : Homogenization.Vec 2) : ‖orderedSpatialJetArray n (Y t) y‖ ≤ gronwallBound 0 L F t

Uniform linear source control for the order-n jet gives a pointwise Gronwall bound at every spatial endpoint.

theorem AVenhance.FaaDiBruno.orderedSpatialJet_norm_le_gronwall_abs {n : ℕ} (hn : 0 < n) {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) (hLip : ∃ (L : ℝ), ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖) {T L F : ℝ} (hsource : ∀ (r : ℝ), |r| ≤ T → ∀ (x : Homogenization.Vec 2), ‖transportSpatialSourceArray n b g Y r x‖ ≤ L * ‖orderedSpatialJetArray n (Y r) x‖ + F) (y : Homogenization.Vec 2) {t : ℝ} (ht : |t| ≤ T) : ‖orderedSpatialJetArray n (Y t) y‖ ≤ gronwallBound 0 L F |t|

The finite-dimensional jet Gronwall estimate for either sign of the target time. The source hypothesis is only needed on the symmetric interval [-T,T].

theorem AVenhance.FaaDiBruno.transportJetArray_coarse_bound {n : ℕ} (hn : 2 ≤ n) {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) {C_f C_g R T : ℝ} (hCf : 0 < C_f) (hCg : 0 ≤ C_g) (hR : 0 < R) (hT : 0 ≤ T) (hTmax : T ≤ 1 / (8 * C_f * R)) (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) (hLower : ∀ (k : ℕ), 1 ≤ k → k < n → ∀ (t : ℝ), |t| ≤ T → snorm (Y t) k (transportShiftRadius C_f R |t|) ≤ ENNReal.ofReal (16 * C_g * |t|)) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (t : ℝ), |t| ≤ T → ∀ (x : Homogenization.Vec 2), ‖orderedSpatialJetArray n (Y t) x‖ ≤ M

theorem AVenhance.FaaDiBruno.transportOrderedPartial_norm_le_symmetric_source_bound {n : ℕ} (hn : 0 < n) {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) (hLip : ∃ (L : ℝ), ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖) {T D : ℝ} (hsource : ∀ (t : ℝ), |t| ≤ T → ∀ (I : Fin n → Fin 2) (x : Homogenization.Vec 2), ‖transportSourceJet (List.ofFn fun (j : Fin n) => coordinateVector 2 (I j)) b g Y (t, x)‖ ≤ D) {t : ℝ} (ht : |t| ≤ T) (I : Fin n → Fin 2) (x : Homogenization.Vec 2) : ‖orderedPartial n (Y t) x I‖ ≤ |t| * D

theorem AVenhance.FaaDiBruno.transportOrderedPartial_norm_le_integrated_source_bound {n : ℕ} (hn : 0 < n) {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) (hLip : ∃ (L : ℝ), ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖) {T t : ℝ} (ht : |t| ≤ T) (B : ℝ → ℝ) (hBcont : Continuous B) (hsource : ∀ (r : ℝ), |r| ≤ T → ∀ (I : Fin n → Fin 2) (x : Homogenization.Vec 2), ‖transportSourceJet (List.ofFn fun (j : Fin n) => coordinateVector 2 (I j)) b g Y (r, x)‖ ≤ B |r|) (I : Fin n → Fin 2) (x : Homogenization.Vec 2) : ‖orderedPartial n (Y t) x I‖ ≤ ∫ (s : ℝ) in 0..|t|, B s

theorem AVenhance.FaaDiBruno.derivativeSup_le_of_orderedPartial_pointwise {n : ℕ} (f : Homogenization.Vec 2 → Homogenization.Vec 2) {M : ℝ} (hpoint : ∀ (I : Fin n → Fin 2) (x : Homogenization.Vec 2), ‖orderedPartial n f x I‖ ≤ M) : derivativeSup n f ≤ ENNReal.ofReal M

A pointwise estimate for every ordered coordinate partial controls the paper's essential-supremum derivative seminorm.