Actual differentiated diffusion energy from two higher scalar gradients.

theorem AVenhance.Infra.Section4.iterate_word_laplacian_gradient_formula {v : Homogenization.Vec 2 → ℝ} (hv : ContDiff ℝ (↑⊤) v) (w : List (Fin 2)) (x : Homogenization.Vec 2) (j : Fin 2) : spaceLap (fun (y : Homogenization.Vec 2) => spaceGrad (iterateSpatialWord w v) y j) x = ∑ k : Fin 2, spaceGrad (iterateSpatialWord (k :: k :: w) v) x j

The Laplacian of an actual gradient is the sum of two twice-differentiated scalar gradients. The order is retained explicitly for the increment induction.

theorem AVenhance.Infra.Section4.iterate_word_laplacian_gradient_sq_bound {v : Homogenization.Vec 2 → ℝ} (hv : ContDiff ℝ (↑⊤) v) (w : List (Fin 2)) (x : Homogenization.Vec 2) : (Homogenization.vecNormSq fun (j : Fin 2) => spaceLap (fun (y : Homogenization.Vec 2) => spaceGrad (iterateSpatialWord w v) y j) x) ≤ 2 * ∑ k : Fin 2, Homogenization.vecNormSq (spaceGrad (iterateSpatialWord (k :: k :: w) v) x)

The actual vector diffusion square is controlled by higher gradient squares.

theorem AVenhance.Infra.Section4.iterate_word_laplacian_gradient_continuousOn {v : ℝ → Homogenization.Vec 2 → ℝ} (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) : ContinuousOn (fun (z : AmnrSpace) (j : Fin 2) => spaceLap (fun (y : Homogenization.Vec 2) => spaceGrad (iterateSpatialWord w (v z.1)) y j) z.2) (Set.Ici 0 ×ˢ Set.univ)

Actual differentiated diffusion has continuous initial-time coefficients.

theorem AVenhance.Infra.Section4.iterate_word_laplacian_gradient_energy_bound {v : ℝ → Homogenization.Vec 2 → ℝ} (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) {G : ℝ} (hE : ∀ (k : Fin 2), (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord (k :: k :: w) (v t))) ≤ G ^ 2) : (spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2) => spaceLap (fun (y : Homogenization.Vec 2) => spaceGrad (iterateSpatialWord w (v t)) y j) x) ≤ 4 * G ^ 2

Actual higher scalar gradient energies bound the differentiated diffusion energy. All natural integrability follows from the actual smooth carrier.