Transport Time Analyticity Estimate

Support for the Armstrong–Vicol anomalous-diffusion formalization.

noncomputable def AVenhance.FaaDiBruno.TransportTimeAnalyticityEstimate.transportTimeRawWeight (m n j k : ℕ) (C_f Q_f R A Q ρ : ℝ) : ℝ

Unnormalized mixed time-space weight in the transport analyticity estimate.

Equations

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

theorem AVenhance.FaaDiBruno.TransportTimeAnalyticityEstimate.transportTime_rawWeight_eq_productBound {m n j k : ℕ} {C_f Q_f R A Q ρ : ℝ} : C_f * Q_f ^ (m - j) * ↑(m - j).factorial * (↑(n - k).factorial * R ^ (n - k) / ↑(n - k + 1) ^ 2) * (A * (↑(k + j + 1).factorial * ↑j.factorial / ↑(k + 1).factorial) * Q ^ j) * (↑(k + 1).factorial * ρ ^ (k + 1) / (↑k + 2) ^ 2) = transportTimeRawWeight m n j k C_f Q_f R A Q ρ

theorem AVenhance.FaaDiBruno.TransportTimeAnalyticityEstimate.transportTime_choose_weight_le {m n j k : ℕ} (hjm : j ≤ m) (hkn : k ≤ n) {C_f Q_f R A Q ρ : ℝ} (hCf : 0 ≤ C_f) (hQf : 0 ≤ Q_f) (hQfQ : Q_f ≤ Q) (hR : 0 < R) (hRρ : R ≤ ρ) (hρ : 0 < ρ) (hA : 0 ≤ A) : ↑(m.choose j) * ↑(n.choose k) * transportTimeRawWeight m n j k C_f Q_f R A Q ρ ≤ C_f * A * ↑m.factorial * ↑n.factorial * Q ^ m * ρ ^ (n + 1) * (↑(k + j + 1).factorial / ↑k.factorial / (↑(n - k + 1) ^ 2 * (↑k + 2) ^ 2))

noncomputable def AVenhance.FaaDiBruno.TransportTimeAnalyticityEstimate.transportTimeFactorialKernel (n j k : ℕ) : ℝ

Factorial convolution kernel for the mixed transport derivative estimate.

Equations

• AVenhance.FaaDiBruno.TransportTimeAnalyticityEstimate.transportTimeFactorialKernel n j k = ↑(k + j + 1).factorial / ↑k.factorial / (↑(n - k + 1) ^ 2 * (↑k + 2) ^ 2)

noncomputable def AVenhance.FaaDiBruno.TransportTimeAnalyticityEstimate.transportTimeScalarKernel (m n j k : ℕ) : ℝ

Normalized scalar convolution kernel for the transport time derivative estimate.

Equations

• AVenhance.FaaDiBruno.TransportTimeAnalyticityEstimate.transportTimeScalarKernel m n j k = (↑n + 1) ^ 2 / (↑(n - k + 1) ^ 2 * (↑k + 2) ^ 2 * (↑m + 1)) * (↑(k + j + 1).factorial / ↑k.factorial)

theorem AVenhance.FaaDiBruno.TransportTimeAnalyticityEstimate.iteratedJointTimeDerivative_shift (m : ℕ) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) : iteratedJointTimeDerivative m (jointTimeDerivative F) = iteratedJointTimeDerivative (m + 1) F

theorem AVenhance.FaaDiBruno.TransportTimeAnalyticityEstimate.directionalJet_mixedTime_successor (m : ℕ) (L : List (Fin 2)) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) F) (p : ℝ × Homogenization.Vec 2) : directionalJet (transportTimeDirections m ++ transportCoordinateDirections L) (jointTimeDerivative F) p = directionalJet (transportTimeDirections (m + 1) ++ transportCoordinateDirections L) F p

theorem AVenhance.FaaDiBruno.TransportTimeAnalyticityEstimate.transportTime_mixedJet_pointwise_bound {m n N M : ℕ} (L : List (Fin 2)) (hL : L.length = 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 Q_f Q_g R A Q ρ : ℝ} (hmM : m ≤ M) (hnN : n ≤ N) (hmnN : m + n + 1 ≤ N) (hCf : 0 < C_f) (hCg : 0 ≤ C_g) (hR : 0 < R) (hρ : 0 < ρ) (hRρ : R ≤ ρ) (hQf : 0 ≤ Q_f) (hQfQ : Q_f ≤ Q) (hQ : 0 < Q) (hQg : 0 ≤ Q_g) (hA : 0 ≤ A) (hB : ∀ (t : ℝ) (u v : ℕ), u ≤ M → v ≤ N → snorm (transportTimeDerivative u (Function.uncurry b) t) v R ≤ ENNReal.ofReal (C_f * Q_f ^ u * ↑u.factorial)) (hG : ∀ (t : ℝ), m ≤ M → n ≤ N → snorm (transportTimeDerivative m (Function.uncurry g) t) n R ≤ ENNReal.ofReal (C_g * Q_g ^ m * ↑m.factorial)) (t : ℝ) (hYlower : ∀ (j k : ℕ), j ≤ m → j + (k + 1) ≤ N → snorm (transportTimeDerivative j (Function.uncurry Y) t) (k + 1) ρ ≤ ENNReal.ofReal (A * (↑(k + 1 + j).factorial * ↑j.factorial / ↑(k + 1).factorial) * Q ^ j)) (x : Homogenization.Vec 2) : ‖directionalJet (transportTimeDirections (m + 1) ++ transportCoordinateDirections L) (Function.uncurry Y) (t, x)‖ ≤ C_g * Q_g ^ m * ↑m.factorial * ↑n.factorial * ρ ^ n / (↑n + 1) ^ 2 + 2 * C_f * A * ↑m.factorial * ↑n.factorial * Q ^ m * ρ ^ (n + 1) * ∑ j ∈ Finset.range (m + 1), ∑ k ∈ Finset.range (n + 1), transportTimeFactorialKernel n j k

theorem AVenhance.FaaDiBruno.TransportTimeAnalyticityEstimate.transportTime_scalarKernels_sum {m n : ℕ} : ∑ j ∈ Finset.range (m + 1), ∑ k ∈ Finset.range (n + 1), transportTimeScalarKernel m n j k = (↑n + 1) ^ 2 / (↑m + 1) * ∑ j ∈ Finset.range (m + 1), ∑ k ∈ Finset.range (n + 1), transportTimeFactorialKernel n j k

theorem AVenhance.FaaDiBruno.TransportTimeAnalyticityEstimate.transportTime_mixedJet_sharp_bound {m n N M : ℕ} (L : List (Fin 2)) (hL : L.length = 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 Q_f Q_g R A Q ρ : ℝ} (hmM : m ≤ M) (hnN : n ≤ N) (hmnN : m + n + 1 ≤ N) (hCf : 0 < C_f) (hCg : 0 ≤ C_g) (hR : 0 < R) (hρ : 0 < ρ) (hRρ : R ≤ ρ) (hρR : ρ ≤ 2 * R) (hQf : 0 ≤ Q_f) (hQfQ : Q_f ≤ Q) (hQg : 0 ≤ Q_g) (hQgQ : Q_g ≤ Q) (hQ1 : C_f * R ≤ Q) (hQ2 : 16 * 2 * C_f * R ≤ Q) (hA0 : 0 ≤ A) (hAeq : A = 2 * C_g / (C_f * R)) (hB : ∀ (t : ℝ) (u v : ℕ), u ≤ M → v ≤ N → snorm (transportTimeDerivative u (Function.uncurry b) t) v R ≤ ENNReal.ofReal (C_f * Q_f ^ u * ↑u.factorial)) (hG : ∀ (t : ℝ), m ≤ M → n ≤ N → snorm (transportTimeDerivative m (Function.uncurry g) t) n R ≤ ENNReal.ofReal (C_g * Q_g ^ m * ↑m.factorial)) (t : ℝ) (hYlower : ∀ (j k : ℕ), j ≤ m → j + (k + 1) ≤ N → snorm (transportTimeDerivative j (Function.uncurry Y) t) (k + 1) ρ ≤ ENNReal.ofReal (A * (↑(k + 1 + j).factorial * ↑j.factorial / ↑(k + 1).factorial) * Q ^ j)) (x : Homogenization.Vec 2) : ‖directionalJet (transportTimeDirections (m + 1) ++ transportCoordinateDirections L) (Function.uncurry Y) (t, x)‖ ≤ A * (↑(n + m + 1).factorial * ↑(m + 1).factorial / ↑n.factorial) * Q ^ (m + 1) * (↑n.factorial * ρ ^ n / (↑n + 1) ^ 2)

theorem AVenhance.FaaDiBruno.TransportTimeAnalyticityEstimate.transportTime_snorm_step {m n N M : ℕ} {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 Q_f Q_g R A Q ρ : ℝ} (hmM : m ≤ M) (hnN : n ≤ N) (hmnN : m + n + 1 ≤ N) (hCf : 0 < C_f) (hCg : 0 ≤ C_g) (hR : 0 < R) (hρ : 0 < ρ) (hRρ : R ≤ ρ) (hρR : ρ ≤ 2 * R) (hQf : 0 ≤ Q_f) (hQfQ : Q_f ≤ Q) (hQg : 0 ≤ Q_g) (hQgQ : Q_g ≤ Q) (hQ1 : C_f * R ≤ Q) (hQ2 : 16 * 2 * C_f * R ≤ Q) (hA0 : 0 ≤ A) (hAeq : A = 2 * C_g / (C_f * R)) (hB : ∀ (t : ℝ) (u v : ℕ), u ≤ M → v ≤ N → snorm (transportTimeDerivative u (Function.uncurry b) t) v R ≤ ENNReal.ofReal (C_f * Q_f ^ u * ↑u.factorial)) (hG : ∀ (t : ℝ), m ≤ M → n ≤ N → snorm (transportTimeDerivative m (Function.uncurry g) t) n R ≤ ENNReal.ofReal (C_g * Q_g ^ m * ↑m.factorial)) (t : ℝ) (hYlower : ∀ (j k : ℕ), j ≤ m → j + (k + 1) ≤ N → snorm (transportTimeDerivative j (Function.uncurry Y) t) (k + 1) ρ ≤ ENNReal.ofReal (A * (↑(k + 1 + j).factorial * ↑j.factorial / ↑(k + 1).factorial) * Q ^ j)) : snorm (transportTimeDerivative (m + 1) (Function.uncurry Y) t) n ρ ≤ ENNReal.ofReal (A * (↑(n + m + 1).factorial * ↑(m + 1).factorial / ↑n.factorial) * Q ^ (m + 1))