Transport ODEApplications

Support for the Armstrong–Vicol anomalous-diffusion formalization.

@[reducible, inline]

abbrev AVenhance.FaaDiBruno.FlowMatrix : Type

Real two-by-two matrices representing spatial flow derivatives.

Equations

• AVenhance.FaaDiBruno.FlowMatrix = (Fin 2 → Fin 2 → ℝ)

def AVenhance.FaaDiBruno.flowMatrixCofactorTranspose (A : FlowMatrix) : FlowMatrix

The transposed cofactor of a two by two matrix.

Equations

• AVenhance.FaaDiBruno.flowMatrixCofactorTranspose A i j = if ↑i = 0 then if ↑j = 0 then A 1 1 else -A 0 1 else if ↑j = 0 then -A 1 0 else A 0 0

theorem AVenhance.FaaDiBruno.TransportODEApplications.flowLinearMap_apply_two (A : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (v : Homogenization.Vec 2) (i : Fin 2) : A v i = A (coordinateVector 2 0) i * v 0 + A (coordinateVector 2 1) i * v 1

theorem AVenhance.FaaDiBruno.TransportODEApplications.flowContinuousLinearMap_det_two (A : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) : A.det = A (coordinateVector 2 0) 0 * A (coordinateVector 2 1) 1 - A (coordinateVector 2 1) 0 * A (coordinateVector 2 0) 1

theorem AVenhance.FaaDiBruno.flow_spatialGradientMatrix_composed_inverse_eq_cofactor {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Infra.Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), Infra.Flow.spatialDivergence b t x = 0) (t : ℝ) (x : Homogenization.Vec 2) : spatialGradientMatrix (fun (y : Homogenization.Vec 2) => X t y 0) (X 0 x t) = flowMatrixCofactorTranspose (spatialGradientMatrix (fun (y : Homogenization.Vec 2) => X 0 y t) x)

For a divergence-free smooth periodic field, the forward flow Jacobian at the inverse point is the transposed cofactor of the inverse-flow Jacobian. This is the finite-dimensional identity used in Proposition p.ODE.flow.

noncomputable def AVenhance.FaaDiBruno.flowCofactorCLM : FlowMatrix →L[ℝ] FlowMatrix

The coordinate cofactor map is linear and does not increase the entrywise sup norm on two by two matrices.

Equations

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

theorem AVenhance.FaaDiBruno.flowCofactorCLM_norm_le : ‖flowCofactorCLM‖ ≤ 1

theorem AVenhance.FaaDiBruno.TransportODEApplications.orderedPartial_postCLM {n : ℕ} (L : FlowMatrix →L[ℝ] FlowMatrix) (f : Homogenization.Vec 2 → FlowMatrix) (hf : ContDiff ℝ (↑n) f) (x : Homogenization.Vec 2) (I : Fin n → Fin 2) : orderedPartial n (fun (y : Homogenization.Vec 2) => L (f y)) x I = L (orderedPartial n f x I)

theorem AVenhance.FaaDiBruno.TransportODEApplications.derivativeSup_postCLM_le {n : ℕ} (L : FlowMatrix →L[ℝ] FlowMatrix) (f : Homogenization.Vec 2 → FlowMatrix) (hf : ContDiff ℝ (↑n) f) (hL : ‖L‖ ≤ 1) : (derivativeSup n fun (x : Homogenization.Vec 2) => L (f x)) ≤ derivativeSup n f

theorem AVenhance.FaaDiBruno.TransportODEApplications.derivativeSup_add_le {n : ℕ} (f g : Homogenization.Vec 2 → FlowMatrix) (hf : ContDiff ℝ (↑n) f) (hg : ContDiff ℝ (↑n) g) : (derivativeSup n fun (x : Homogenization.Vec 2) => f x + g x) ≤ derivativeSup n f + derivativeSup n g

theorem AVenhance.FaaDiBruno.TransportODEApplications.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.TransportODEApplications.snorm_postCLM_le {n : ℕ} {R : ℝ} (L : FlowMatrix →L[ℝ] FlowMatrix) (f : Homogenization.Vec 2 → FlowMatrix) (hf : ContDiff ℝ (↑n) f) (hL : ‖L‖ ≤ 1) : snorm (fun (x : Homogenization.Vec 2) => L (f x)) n R ≤ snorm f n R

theorem AVenhance.FaaDiBruno.TransportODEApplications.snorm_add_le {n : ℕ} {R : ℝ} (f g : Homogenization.Vec 2 → FlowMatrix) (hf : ContDiff ℝ (↑n) f) (hg : ContDiff ℝ (↑n) g) : snorm (fun (x : Homogenization.Vec 2) => f x + g x) n R ≤ snorm f n R + snorm g n R

theorem AVenhance.FaaDiBruno.TransportODEApplications.snorm_const_matrix_le_one (n : ℕ) (R : ℝ) : snorm (fun (x : Homogenization.Vec 2) (i j : Fin 2) => if i = j then 1 else 0) n R ≤ ENNReal.ofReal 1

theorem AVenhance.FaaDiBruno.TransportODEApplications.flowMatrixCofactor_add_identity (A : FlowMatrix) : (flowMatrixCofactorTranspose fun (i j : Fin 2) => (if i = j then 1 else 0) + A i j) = fun (i j : Fin 2) => (if i = j then 1 else 0) + flowMatrixCofactorTranspose A i j

theorem AVenhance.FaaDiBruno.flow_inverse_displacement_isTransportSolution_of_jointSmooth {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) : IsClassicalTransportSolution b (fun (t : ℝ) (x : Homogenization.Vec 2) => -b t x) fun (t : ℝ) (x : Homogenization.Vec 2) => X 0 x t - x

If the full time-space flow is smooth, its inverse displacement solves the backward transport equation with source -b. The remaining flow-ODE regularity task is to derive this smoothness witness from IsFlow.

theorem AVenhance.FaaDiBruno.flow_spatialFirstOrder_snorm_Dn_base {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) {C_f R_f : ℝ} (hCf : 0 < C_f) (hRf : 0 < R_f) (hB : ∀ (r : ℝ) (k : ℕ), 1 ≤ k → k ≤ N → snorm (b r) k R_f ≤ ENNReal.ofReal C_f) {t : ℝ} (ht : |t| ≤ 1 / (8 * C_f * R_f)) : snorm (fun (x : Homogenization.Vec 2) => X t x 0) 1 (8 * 2 * R_f * (1 + 8 * 2 * C_f * R_f * |t|)) ≤ ENNReal.ofReal (1 / (2 * 2 * R_f))

The n=1 induction base used in Proposition p.ODE.flow.2, specialized to dimension two. It uses only the paper's order-one field seminorm bound and does not require divergence freeness.

noncomputable def AVenhance.FaaDiBruno.flowHalfBinomialCoeff (n : ℕ) : ℝ

The positive coefficient in the paper's signed half-binomial induction, with index n corresponding to derivative order n+1.

Equations

• AVenhance.FaaDiBruno.flowHalfBinomialCoeff n = (-1) ^ n * Ring.choose (1 / 2) (n + 1)

theorem AVenhance.FaaDiBruno.flowHalfBinomialCoeff_one : flowHalfBinomialCoeff 1 = 1 / 8

theorem AVenhance.FaaDiBruno.flowHalfBinomialCoeff_succ (n : ℕ) : flowHalfBinomialCoeff (n + 1) = (↑n + 1 / 2) / (↑n + 2) * flowHalfBinomialCoeff n

theorem AVenhance.FaaDiBruno.flowHalfBinomialCoeff_nonneg {n : ℕ} (hn : 1 ≤ n) : 0 ≤ flowHalfBinomialCoeff n

theorem AVenhance.FaaDiBruno.flowHalfBinomialCoeff_le_inverse {n : ℕ} (hn : 1 ≤ n) : flowHalfBinomialCoeff n ≤ 1 / (4 * (↑n + 1))

theorem AVenhance.FaaDiBruno.flow_orderedPartial_hasDerivAt {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) (s t : ℝ) (x : Homogenization.Vec 2) {n : ℕ} (I : Fin n → Fin 2) : HasDerivAt (fun (r : ℝ) => orderedPartial n (fun (y : Homogenization.Vec 2) => X r y s) x I) (orderedPartial n (fun (y : Homogenization.Vec 2) => b t (X t y s)) x I) t

Along a jointly smooth flow, every ordered spatial coordinate jet obeys the time derivative obtained by applying the same jet to the vector field composed with the flow.

theorem AVenhance.FaaDiBruno.flow_spatialGradient_snorm_of_Dn {n : ℕ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {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 A : ℝ} (hCf : 0 < C_f) (hRf : 0 < R_f) (hA : 0 ≤ A) (hAhalf : 4 * A ≤ 1 / (↑n + 1)) {t : ℝ} (ht : |t| ≤ 1 / (8 * C_f * R_f)) (hDn : snorm (fun (x : Homogenization.Vec 2) => X t x 0) (n + 1) (8 * 2 * R_f * (1 + 8 * 2 * C_f * R_f * |t|)) ≤ ENNReal.ofReal (A / (2 * 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

The final reduction step in p.ODE.flow.2: the paper's level n+1 bound on the flow itself implies its level-n gradient bound. The input coefficient is the signed half-binomial coefficient, for which 4 * A ≤ 1 / (n + 1); the resulting dimension-two bound is at most 6, hence the paper's target 12.

theorem AVenhance.FaaDiBruno.flow_spatialGradient_snorm_of_flowDn {n : ℕ} (hn : 1 ≤ n) {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {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) {t : ℝ} (ht : |t| ≤ 1 / (8 * C_f * R_f)) (hDn : snorm (fun (x : Homogenization.Vec 2) => X t x 0) (n + 1) (8 * 2 * R_f * (1 + 8 * 2 * C_f * R_f * |t|)) ≤ ENNReal.ofReal (flowHalfBinomialCoeff n / (2 * 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

The reduction in p.ODE.flow.2 with the paper's actual signed half-binomial coefficient at order n+1.

theorem AVenhance.FaaDiBruno.flow_inverse_displacement_at_start_isTransportSolution_of_jointSmooth {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) (s : ℝ) : IsClassicalTransportSolution (fun (t : ℝ) (x : Homogenization.Vec 2) => b (s + t) x) (fun (t : ℝ) (x : Homogenization.Vec 2) => -b (s + t) x) fun (t : ℝ) (x : Homogenization.Vec 2) => X s x (s + t) - x

For an arbitrary starting time, the inverse displacement solves the transport equation for the time-shifted velocity. This is the characteristic identity needed to apply Lemma 10577 at each center s in the stream recursion; the smoothness witness remains explicit.