Positive Time

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.FaaDiBruno.PositiveTime.flowDirectionalJet_id_constant (I : List (Homogenization.Vec 2)) (hI : I ≠ []) : ∃ (c : Homogenization.Vec 2), (directionalJet I fun (x : Homogenization.Vec 2) => x) = fun (x : Homogenization.Vec 2) => c

theorem AVenhance.FaaDiBruno.PositiveTime.flowOrderedPartial_id_eq_zero {n : ℕ} (hn : 2 ≤ n) (x : Homogenization.Vec 2) (I : Fin n → Fin 2) : orderedPartial n (fun (y : Homogenization.Vec 2) => y) x I = 0

theorem AVenhance.FaaDiBruno.PositiveTime.flowIntegralAffinePow {t B : ℝ} (_ht : 0 ≤ t) (hB : 0 < B) (n : ℕ) : ∫ (s : ℝ) in 0..t, (1 + B * s) ^ n = ((1 + B * t) ^ (n + 1) - 1) / (B * (↑n + 1))

theorem AVenhance.FaaDiBruno.PositiveTime.flowLinearODE_norm_bound {t L B K : ℝ} {n : ℕ} (ht : 0 < t) (hL : 0 ≤ L) (hB : 0 < B) (hK : 0 ≤ K) (A : ℝ → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (f y : ℝ → Homogenization.Vec 2) (hAcontinuous : Continuous A) (hfcontinuous : Continuous f) (hycontinuous : Continuous y) (hAbound : ∀ (s : ℝ), ‖A s‖ ≤ L) (hfbound : ∀ s ∈ Set.Icc 0 t, ‖f s‖ ≤ K * (1 + B * s) ^ n) (hderiv : ∀ s ∈ Set.Icc 0 t, HasDerivAt y ((A s) (y s) + f s) s) (hy0 : y 0 = 0) : ‖y t‖ ≤ K * (((1 + B * t) ^ (n + 1) - 1) / (B * (↑n + 1))) * Real.exp (L * t)

theorem AVenhance.FaaDiBruno.PositiveTime.flowExpOneSixteenth_le_fourThirds : Real.exp (1 / 16) ≤ 4 / 3

theorem AVenhance.FaaDiBruno.PositiveTime.flowDn_coordinate_positive_bound {N n : ℕ} (hn : 2 ≤ n) (hnN : n ≤ N) {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Infra.Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (hXsmooth : ContDiff ℝ ↑⊤ fun (p : (ℝ × Homogenization.Vec 2) × ℝ) => X p.1.1 p.1.2 p.2) {C_f R_f : ℝ} (hCf : 0 < C_f) (hRf : 0 < R_f) (hBfield : ∀ (s : ℝ) (k : ℕ), 1 ≤ k → k ≤ N → snorm (b s) k R_f ≤ ENNReal.ofReal C_f) {t : ℝ} (ht : 0 < t) (htT : t ≤ 1 / (8 * C_f * R_f)) (hLower : ∀ (s : ℝ), 0 ≤ s → s ≤ 1 / (8 * C_f * R_f) → ∀ (k : ℕ), 1 ≤ k → k < n → snorm (fun (y : Homogenization.Vec 2) => X s y 0) k (8 * 2 * R_f * (1 + 8 * 2 * C_f * R_f * s)) ≤ ENNReal.ofReal (flowHalfBinomialCoeff (k - 1) / (2 * R_f))) (I : Fin n → Fin 2) (x : Homogenization.Vec 2) : ‖orderedPartial n (fun (y : Homogenization.Vec 2) => X t y 0) x I‖ ≤ flowHalfBinomialCoeff (n - 1) / (2 * R_f) * ↑n.factorial * (8 * 2 * R_f * (1 + 8 * 2 * C_f * R_f * t)) ^ n / (↑n + 1) ^ 2

Pointwise closure of the order-n flow jet equation on positive time. This is the exact factorial/radius comparison in the paper's induction.

theorem AVenhance.FaaDiBruno.flow_spatialDn_snorm_positive {N : ℕ} (hN : 1 ≤ N) {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Infra.Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (hXsmooth : ContDiff ℝ ↑⊤ fun (p : (ℝ × Homogenization.Vec 2) × ℝ) => X p.1.1 p.1.2 p.2) {C_f R_f : ℝ} (hCf : 0 < C_f) (hRf : 0 < R_f) (hBfield : ∀ (s : ℝ) (k : ℕ), 1 ≤ k → k ≤ N → snorm (b s) k R_f ≤ ENNReal.ofReal C_f) (n : ℕ) : 1 ≤ n → n ≤ N → ∀ (t : ℝ), 0 ≤ t → t ≤ 1 / (8 * C_f * R_f) → snorm (fun (y : Homogenization.Vec 2) => X t y 0) n (8 * 2 * R_f * (1 + 8 * 2 * C_f * R_f * t)) ≤ ENNReal.ofReal (flowHalfBinomialCoeff (n - 1) / (2 * R_f))

The positive-time seminorm induction in p.ODE.flow.2, retaining the paper's coefficient at every derivative order.