Spatial derivative transfer for the current material diffusion term.

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

theorem AVenhance.Infra.Section4.iterate_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.iterate_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.iterate_laplacian_smooth {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (spaceLap f)

theorem AVenhance.Infra.Section4.iterate_classical_material_gradient_equation {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F u : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ F u₀ u) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) (hF : DifferentiableAt ℝ (F t) x) (i : Fin 2) : spaceGrad (amnrMaterial b u t) x i = κ * spaceLap (fun (y : Homogenization.Vec 2) => spaceGrad (u t) y i) x + spaceGrad (F t) x i

Differentiate the actual material PDE in space, commuting diffusion with one coordinate derivative. No material-gradient equation is assumed.

theorem AVenhance.Infra.Section4.iterate_gradient_periodic {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hper : IsZ2Periodic f) : IsZ2Periodic (spaceGrad f)