Characteristic identities for smooth solutions of the transport equation.

noncomputable def AVenhance.FaaDiBruno.spatialDerivativeCLM (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

Restrict the derivative of a joint time-space field to its spatial directions.

Equations

• AVenhance.FaaDiBruno.spatialDerivativeCLM F t x = fderiv ℝ F (t, x) ∘SL ContinuousLinearMap.inr ℝ ℝ (Homogenization.Vec 2)

theorem AVenhance.FaaDiBruno.spatialDerivativeCLM_eq_slice {f : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContDiff ℝ 1 (Function.uncurry f)) (t : ℝ) (x : Homogenization.Vec 2) : spatialDerivativeCLM (Function.uncurry f) t x = fderiv ℝ (f t) x

Restricting a smooth joint derivative to the spatial factor agrees with the derivative of the fixed-time slice.

theorem AVenhance.FaaDiBruno.derivativeSup_one_le_of_fderiv_norm_le {d : ℕ} [Nonempty (Fin d)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec d → F) (hf : ContDiff ℝ 1 f) {M : ℝ} (hD : ∀ (x : Homogenization.Vec d), ‖fderiv ℝ f x‖ ≤ M) : derivativeSup 1 f ≤ ENNReal.ofReal M

A pointwise operator bound for the first derivative bounds the paper's order-one coordinate seminorm, including vector-valued outputs.

theorem AVenhance.FaaDiBruno.snorm_one_le_of_derivativeSup_le {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec d → F) {R M : ℝ} (hR : 0 < R) (hD : derivativeSup 1 f ≤ ENNReal.ofReal M) : snorm f 1 R ≤ ENNReal.ofReal (4 * M / R)

Convert a pointwise order-one derivative bound into the normalized order-one seminorm bound, with the paper's factor 4 / R.

structure AVenhance.FaaDiBruno.IsClassicalTransportSolution (b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : Prop

A classical solution of ∂ₜY + b·∇Y = g with zero initial data. The directional derivative formulation keeps the statement coordinate-free.

• smooth : ContDiff ℝ (↑⊤) (Function.uncurry Y)
• equation (t : ℝ) (x : Homogenization.Vec 2) : (fderiv ℝ (Function.uncurry Y) (t, x)) (1, b t x) = g t x
• initial (x : Homogenization.Vec 2) : Y 0 x = 0

theorem AVenhance.FaaDiBruno.transportSolution_spatialDerivative_equation {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (t : ℝ) (x v : Homogenization.Vec 2) : (fderiv ℝ (fun (q : ℝ × Homogenization.Vec 2) => (fderiv ℝ (Function.uncurry Y) q) (0, v)) (t, x)) (1, b t x) = (fderiv ℝ (Function.uncurry g) (t, x)) (0, v) - (fderiv ℝ (Function.uncurry Y) (t, x)) (0, (fderiv ℝ (Function.uncurry b) (t, x)) (0, v))

Differentiating the transport equation in a spatial direction gives the linear transport equation for that directional derivative.

noncomputable def AVenhance.FaaDiBruno.transportDirectionalDerivative (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (v : Homogenization.Vec 2) : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2

The joint-space function obtained by differentiating a field in one fixed spatial direction.

Equations

• AVenhance.FaaDiBruno.transportDirectionalDerivative F v p = (fderiv ℝ F p) (0, v)

theorem AVenhance.FaaDiBruno.transportSolution_directionalDerivative_isSolution {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (hg : ContDiff ℝ (↑⊤) (Function.uncurry g)) (v : Homogenization.Vec 2) : IsClassicalTransportSolution b (fun (t : ℝ) (x : Homogenization.Vec 2) => transportDirectionalDerivative (Function.uncurry g) v (t, x) - (fderiv ℝ (Function.uncurry Y) (t, x)) (0, (fderiv ℝ (Function.uncurry b) (t, x)) (0, v))) fun (t : ℝ) (x : Homogenization.Vec 2) => transportDirectionalDerivative (Function.uncurry Y) v (t, x)

Differentiating a classical transport solution once in a fixed spatial direction again gives a classical transport solution. The differentiated source includes the commutator with the spatial derivative of the drift.

structure AVenhance.FaaDiBruno.IsSmoothClassicalTransportSolution (b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) extends AVenhance.FaaDiBruno.IsClassicalTransportSolution b g Y : Prop

A smooth transport solution that also records smoothness of its source. The source smoothness field lets us iterate spatial differentiation.

• smooth : ContDiff ℝ (↑⊤) (Function.uncurry Y)
• equation (t : ℝ) (x : Homogenization.Vec 2) : (fderiv ℝ (Function.uncurry Y) (t, x)) (1, b t x) = g t x
• initial (x : Homogenization.Vec 2) : Y 0 x = 0
• source_smooth : ContDiff ℝ (↑⊤) (Function.uncurry g)

theorem AVenhance.FaaDiBruno.transportDirectionalSource_contDiff {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (hg : ContDiff ℝ (↑⊤) (Function.uncurry g)) (v : Homogenization.Vec 2) : ContDiff ℝ (↑⊤) (Function.uncurry fun (t : ℝ) (x : Homogenization.Vec 2) => transportDirectionalDerivative (Function.uncurry g) v (t, x) - (fderiv ℝ (Function.uncurry Y) (t, x)) (0, (fderiv ℝ (Function.uncurry b) (t, x)) (0, v)))

Smoothness of the source obtained by differentiating the transport equation once in a spatial direction.

theorem AVenhance.FaaDiBruno.transportSolution_directionalDerivative_isSmoothSolution {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hY : IsSmoothClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) (v : Homogenization.Vec 2) : IsSmoothClassicalTransportSolution b (fun (t : ℝ) (x : Homogenization.Vec 2) => transportDirectionalDerivative (Function.uncurry g) v (t, x) - (fderiv ℝ (Function.uncurry Y) (t, x)) (0, (fderiv ℝ (Function.uncurry b) (t, x)) (0, v))) fun (t : ℝ) (x : Homogenization.Vec 2) => transportDirectionalDerivative (Function.uncurry Y) v (t, x)

The one-step derivative theorem upgraded to preserve smoothness of its new source, so it can be iterated any finite number of times.

def AVenhance.FaaDiBruno.transportSpatialJet (I : List (Homogenization.Vec 2)) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2

The joint field of the iterated spatial derivative in a finite ordered list of fixed directions.

Equations

• AVenhance.FaaDiBruno.transportSpatialJet [] F = F
• AVenhance.FaaDiBruno.transportSpatialJet (v :: J) F = AVenhance.FaaDiBruno.transportDirectionalDerivative (AVenhance.FaaDiBruno.transportSpatialJet J F) v

def AVenhance.FaaDiBruno.transportSourceJet (I : List (Homogenization.Vec 2)) (b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2

The recursively differentiated source in the transport equation.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.FaaDiBruno.transportSourceJet [] b g Y = Function.uncurry g

theorem AVenhance.FaaDiBruno.transportSolution_iteratedDirectionalDerivative_isSmoothSolution {b g Y : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (I : List (Homogenization.Vec 2)) (hY : IsSmoothClassicalTransportSolution b g Y) (hb : ContDiff ℝ (↑⊤) (Function.uncurry b)) : IsSmoothClassicalTransportSolution b (Function.curry (transportSourceJet I b g Y)) (Function.curry (transportSpatialJet I (Function.uncurry Y)))

Every finite ordered spatial derivative of a smooth classical transport solution solves the correspondingly differentiated transport equation. The source recursion explicitly retains all commutator terms.