Spatial diffusion calculus below the public AMNR facade.

theorem AVenhance.Infra.Section4.amnr_energy_gradient_smooth {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (spaceGrad f)

theorem AVenhance.Infra.Section4.amnr_energy_coordinate_derivatives_commute {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i j : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad f y i) x j = spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad f y j) x i

theorem AVenhance.Infra.Section4.amnr_energy_gradient_laplacian_commute {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec 2) (i : Fin 2) : spaceGrad (spaceLap f) x i = spaceLap (fun (y : Homogenization.Vec 2) => spaceGrad f y i) x

The gradient of the Laplacian is the componentwise Laplacian of the gradient. This justifies moving current diffusion derivatives to the preceding increment in the oscillatory material pairing.

theorem AVenhance.Infra.Section4.amnr_energy_laplacian_smooth {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (spaceLap f)