Ordered spatial words and exact diffusion commutation for l.V.

def AVenhance.Infra.Section4.iterateSpatialWord : List (Fin 2) → (Homogenization.Vec 2 → ℝ) → Homogenization.Vec 2 → ℝ

Ordered coordinate derivatives, with the outermost derivative first.

Equations

• AVenhance.Infra.Section4.iterateSpatialWord [] x✝ = x✝
• AVenhance.Infra.Section4.iterateSpatialWord (i :: w) x✝ = fun (x : Homogenization.Vec 2) => AVenhance.spaceGrad (AVenhance.Infra.Section4.iterateSpatialWord w x✝) x i

theorem AVenhance.Infra.Section4.iterateSpatialWord_smooth {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (w : List (Fin 2)) : ContDiff ℝ (↑⊤) (iterateSpatialWord w f)

Classical spatial smoothness is preserved at every derivative order.

theorem AVenhance.Infra.Section4.iterateSpatialWord_laplacian {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (w : List (Fin 2)) : iterateSpatialWord w (spaceLap f) = spaceLap (iterateSpatialWord w f)

Constant diffusivity commutes with every ordered spatial derivative. No differentiated diffusion equation is supplied as an induction hypothesis.