Exact all-order drift commutators, before quantitative norm estimates.

noncomputable def AVenhance.Infra.Section4.iterateVelocityCommutator (b : AmnrSpace → Homogenization.Vec 2) (i : Fin 2) (f : AmnrSpace → ℝ) (z : AmnrSpace) : ℝ

The one-coordinate drift commutator applied to the actual scalar field.

Equations

• AVenhance.Infra.Section4.iterateVelocityCommutator b i f z = (fderiv ℝ f z) (0, (fderiv ℝ b z) (0, Homogenization.basisVec i))

def AVenhance.Infra.Section4.iterateWordMaterialError (b : AmnrSpace → Homogenization.Vec 2) : List (Fin 2) → (AmnrSpace → ℝ) → AmnrSpace → ℝ

Ordered commutator expansion. The outer derivative differentiates all previous errors, and the new error differentiates the actual velocity once.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section4.iterateWordMaterialError b [] x✝ = fun (x : AVenhance.Infra.Section4.AmnrSpace) => 0

theorem AVenhance.Infra.Section4.iterate_amnrWord_smoothOn {U : Set AmnrSpace} (hU : IsOpen U) {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiffOn ℝ (↑⊤) b U) (hf : ContDiffOn ℝ (↑⊤) f U) (w : List (Option (Fin 2))) : ContDiffOn ℝ (↑⊤) (amnrWord b w f) U

Finite words preserve smoothness on an open space-time domain.

theorem AVenhance.Infra.Section4.iterateVelocityCommutator_smoothOn {U : Set AmnrSpace} (hU : IsOpen U) {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiffOn ℝ (↑⊤) b U) (hf : ContDiffOn ℝ (↑⊤) f U) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (iterateVelocityCommutator b i f) U

The velocity commutator is a smooth, explicitly differentiated field.

theorem AVenhance.Infra.Section4.iterateWordMaterialError_smoothOn {U : Set AmnrSpace} (hU : IsOpen U) {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiffOn ℝ (↑⊤) b U) (hf : ContDiffOn ℝ (↑⊤) f U) (w : List (Fin 2)) : ContDiffOn ℝ (↑⊤) (iterateWordMaterialError b w f) U

Every recursively expanded error is smooth; this justifies differentiating its sum in the next induction step rather than assuming a commutator equation.

theorem AVenhance.Infra.Section4.iterate_spatial_word_material_expansion {U : Set AmnrSpace} (hU : IsOpen U) {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiffOn ℝ (↑⊤) b U) (hf : ContDiffOn ℝ (↑⊤) f U) (w : List (Fin 2)) : Set.EqOn (amnrWord b (List.map some w) (amnrOp b none f)) (fun (z : AmnrSpace) => amnrOp b none (amnrWord b (List.map some w) f) z + iterateWordMaterialError b w f z) U

Commute the actual material operator past any ordered spatial word. The entire drift error is the explicit recursive expansion above.