A quantitative first-order estimate for the spatial derivative of a flow.

def AVenhance.Infra.Flow.GradientDeviation.gradientReverseTimeField (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2

Reverse-time vector field used in the gradient-deviation estimate.

Equations

• AVenhance.Infra.Flow.GradientDeviation.gradientReverseTimeField b t x = -b (-t) x

def AVenhance.Infra.Flow.GradientDeviation.gradientReverseTimeFlow (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2

Reverse-time flow used in the gradient-deviation estimate.

Equations

• AVenhance.Infra.Flow.GradientDeviation.gradientReverseTimeFlow X t x s = X (-t) x (-s)

theorem AVenhance.Infra.Flow.GradientDeviation.gradientReverseTimeField_smoothPeriodic {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) : SmoothPeriodicField (gradientReverseTimeField b)

theorem AVenhance.Infra.Flow.GradientDeviation.gradientReverseTimeFlow_isFlow {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : IsFlow (gradientReverseTimeField b) (gradientReverseTimeFlow X)

theorem AVenhance.Infra.Flow.GradientDeviation.gradientReverseTimeField_derivBound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {L : ℝ} (hL : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖jointSpatialFDeriv b r y‖ ≤ L) (r : ℝ) (y : Homogenization.Vec 2) : ‖jointSpatialFDeriv (gradientReverseTimeField b) r y‖ ≤ L

The spatial derivative bound is unchanged by time reversal.

theorem AVenhance.Infra.Flow.flow_fderiv_deviation_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {L : ℝ} (hL_nonneg : 0 ≤ L) (hL : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖jointSpatialFDeriv b r y‖ ≤ L) {s t : ℝ} (hst : s ≤ t) (x : Homogenization.Vec 2) : ‖fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) x - 1‖ ≤ Real.exp (L * (t - s)) - 1

If the spatial derivative of a smooth periodic field is bounded by L, then the spatial derivative of its forward flow differs from the identity by at most exp (L (t-s)) - 1.

theorem AVenhance.Infra.Flow.flow_fderiv_deviation {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {L : ℝ} (hL_nonneg : 0 ≤ L) (hL : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖jointSpatialFDeriv b r y‖ ≤ L) (s t : ℝ) (x : Homogenization.Vec 2) : ‖fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) x - 1‖ ≤ Real.exp (L * |t - s|) - 1

The exponential first-derivative estimate holds on either side of the initial time.

theorem AVenhance.Infra.Flow.flow_fderiv_deviation_of_small_time {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {L : ℝ} (hL_nonneg : 0 ≤ L) (hL : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖jointSpatialFDeriv b r y‖ ≤ L) (s t : ℝ) (x : Homogenization.Vec 2) (ht : L * |t - s| ≤ 1) : ‖fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) x - 1‖ ≤ 2 * L * |t - s|

On the unit exponential scale, exp(z)-1 ≤ 2z; this is the linear small-time form used in (10814)-(10818).

theorem AVenhance.Infra.Flow.flow_fderiv_deviation_paper_bound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {d : ℕ} {C_f R_f : ℝ} (hd : 1 ≤ d) (hCf : 0 < C_f) (hRf : 0 < R_f) (hDb : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖jointSpatialFDeriv b r y‖ ≤ ↑d * C_f * R_f / 4) {t : ℝ} (ht : |t| ≤ 1 / (4 * ↑d * C_f * R_f)) (x : Homogenization.Vec 2) : ‖fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y 0) x - 1‖ ≤ ↑d * C_f * R_f * |t| ∧ ↑d * C_f * R_f * |t| ≤ 1 / 4

The gradient-deviation estimate in (10814)-(10818), once the seminorm hypothesis has been converted to the pointwise derivative bound ‖Dₓb‖ ≤ d C_f R_f / 4.

theorem AVenhance.Infra.Flow.jointSpatialFDeriv_bound_of_snorm {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {C_f R_f : ℝ} (hCf : 0 < C_f) (hRf : 0 < R_f) (hs : ∀ (r : ℝ), FaaDiBruno.snorm (b r) 1 R_f ≤ ENNReal.ofReal C_f) (r : ℝ) (y : Homogenization.Vec 2) : ‖jointSpatialFDeriv b r y‖ ≤ 2 * C_f * R_f / 4

Convert the paper's order-one seminorm hypothesis for a smooth Vec 2 field into the pointwise spatial derivative bound used in (10814)-(10818).

theorem AVenhance.Infra.Flow.flow_fderiv_deviation_of_snorm {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {C_f R_f : ℝ} (hCf : 0 < C_f) (hRf : 0 < R_f) (hs : ∀ (r : ℝ), FaaDiBruno.snorm (b r) 1 R_f ≤ ENNReal.ofReal C_f) {t : ℝ} (ht : |t| ≤ 1 / (4 * 2 * C_f * R_f)) (x : Homogenization.Vec 2) : ‖fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y 0) x - 1‖ ≤ 2 * C_f * R_f * |t| ∧ 2 * C_f * R_f * |t| ≤ 1 / 4

The gradient estimate in Proposition p.ODE.flow (10811)-(10825), with the paper's seminorm assumption supplying the derivative bound.