Explicit spatial/material commutators used in the temperature cascade.

theorem AVenhance.Infra.Section4.amnrWord_contDiffOn_infty {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

Every finite ordered word preserves classical smoothness on an open domain.

theorem AVenhance.Infra.Section4.amnrVelocityGradient_contDiffOn_infty {U : Set AmnrSpace} (hU : IsOpen U) {b : AmnrSpace → Homogenization.Vec 2} (hb : ContDiffOn ℝ (↑⊤) b U) (i p : Fin 2) : ContDiffOn ℝ (↑⊤) (amnrVelocityGradient b i p) U

Primitive velocity gradients are smooth from the velocity itself.

theorem AVenhance.Infra.Section4.amnrWord_spatial_independent (b c : AmnrSpace → Homogenization.Vec 2) (α : List (Fin 2)) (f : AmnrSpace → ℝ) : amnrWord b (List.map some α) f = amnrWord c (List.map some α) f

Pure spatial words do not depend on the velocity chosen for the material letter, so diffusion can be written with the actual advecting field.