Natural all-order forcing integrability from actual coefficient jets.

theorem AVenhance.Infra.Section4.iterate_word_forcing_gradient_continuousOn {A : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : ℝ → Homogenization.Vec 2 → ℝ} (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hA : ∀ (t : ℝ), 0 ≤ t → ContDiff ℝ (↑⊤) (A t)) (hcoef : ∀ (r : List (Fin 2)), ContinuousOn (fun (z : AmnrSpace) => iterateMatrixWord (A z.1) r z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) : ContinuousOn (fun (z : AmnrSpace) => spaceGrad (iterateSpatialWord w (vecDiv fun (y : Homogenization.Vec 2) => (A z.1 y).mulVec (spaceGrad (v z.1) y))) z.2) (Set.Ici 0 ×ˢ Set.univ)

Joint continuity of the actual forcing gradient follows from its finite explicit word-flux expansion, including the initial boundary.

theorem AVenhance.Infra.Section4.iterate_word_forcing_gradient_energy_integrable {A : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : ℝ → Homogenization.Vec 2 → ℝ} (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hA : ∀ (t : ℝ), 0 ≤ t → ContDiff ℝ (↑⊤) (A t)) (hcoef : ∀ (r : List (Fin 2)), ContinuousOn (fun (z : AmnrSpace) => iterateMatrixWord (A z.1) r z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) : MeasureTheory.IntegrableOn (fun (z : AmnrSpace) => Homogenization.vecNormSq (spaceGrad (iterateSpatialWord w (vecDiv fun (y : Homogenization.Vec 2) => (A z.1 y).mulVec (spaceGrad (v z.1) y))) z.2)) timeCube MeasureTheory.volume

No forcing-energy integrability premise is needed for the actual smooth coefficient and scalar carriers.