Small Time

Support for the Armstrong–Vicol anomalous-diffusion formalization.

def AVenhance.FaaDiBruno.SmallTime.flowDnReverseField (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2

Vector field obtained by reversing time and negating the velocity.

Equations

• AVenhance.FaaDiBruno.SmallTime.flowDnReverseField b t x = -b (-t) x

def AVenhance.FaaDiBruno.SmallTime.flowDnReverseFlow (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2

Flow obtained by reversing both its observation time and its starting time.

Equations

• AVenhance.FaaDiBruno.SmallTime.flowDnReverseFlow X t x s = X (-t) x (-s)

theorem AVenhance.FaaDiBruno.SmallTime.flowDnReverseField_smoothPeriodic {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Infra.Flow.SmoothPeriodicField b) : Infra.Flow.SmoothPeriodicField (flowDnReverseField b)

theorem AVenhance.FaaDiBruno.SmallTime.flowDnReverseFlow_isFlow {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : IsFlow (flowDnReverseField b) (flowDnReverseFlow X)

theorem AVenhance.FaaDiBruno.SmallTime.flowDn_snorm_neg_eq {n : ℕ} {R : ℝ} (f : Homogenization.Vec 2 → Homogenization.Vec 2) : snorm (fun (x : Homogenization.Vec 2) => -f x) n R = snorm f n R

theorem AVenhance.FaaDiBruno.flow_spatialDn_snorm_smallTime {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) {t : ℝ} (ht : |t| ≤ 1 / (8 * C_f * R_f)) (n : ℕ) (hn : 1 ≤ n) (hnN : n ≤ N) : 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 signed-time version of the paper's all-order flow seminorm estimate. Time reversal preserves both the field hypotheses and the exact coefficient.

theorem AVenhance.FaaDiBruno.flow_spatialGradient_snorm_paper {N n : ℕ} (hn : 1 ≤ n) (hnN : n + 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) {t : ℝ} (ht : |t| ≤ 1 / (8 * C_f * R_f)) : snorm (spatialGradientMatrix fun (y : Homogenization.Vec 2) => X t y 0) n (8 * 2 * R_f * (1 + 8 * 2 * C_f * R_f * |t|)) ≤ ENNReal.ofReal 12

Consumed form of Proposition p.ODE.flow.2 in dimension two. The joint-smoothness witness is explicit until the flow regularity is established.