Exact forcing and drift pairings for the all-order differentiated energy.

theorem AVenhance.Infra.Section4.iterate_divergence_smooth {H : Homogenization.Vec 2 → Homogenization.Vec 2} (hH : ContDiff ℝ (↑⊤) H) : ContDiff ℝ (↑⊤) (vecDiv H)

Smooth fluxes have smooth divergence.

theorem AVenhance.Infra.Section4.iterate_divergence_product_integrable {u : Homogenization.Vec 2 → ℝ} {H : Homogenization.Vec 2 → Homogenization.Vec 2} (hu : ContDiff ℝ (↑⊤) u) (hH : ContDiff ℝ (↑⊤) H) : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => u x * vecDiv H x) unitCube MeasureTheory.volume

Every smooth divergence pairing on the cell is integrable.

theorem AVenhance.Infra.Section4.iterate_word_forcing_drift_pairing {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)) {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hv : ContDiff ℝ (↑⊤) v) (hAp : IsZ2Periodic A) (hvp : IsZ2Periodic v) {t : ℝ} (ht : 0 < t) (hup : IsZ2Periodic (u t)) (w : List (Fin 2)) : ∫ (x : Homogenization.Vec 2) in unitCube, iterateSpatialWord w (u t) x * (iterateSpatialWord w (vecDiv fun (y : Homogenization.Vec 2) => (A y).mulVec (spaceGrad v y)) x - iterateWordMaterialError (fun (z : AmnrSpace) => streamVel φ z.1 z.2) w (fun (z : AmnrSpace) => u z.1 z.2) (t, x)) = (-∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u t)) x) (iterateWordFlux A v w x)) - ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u t)) x) (iterateWordFlux (fun (y : Homogenization.Vec 2) => φ t y • sigmaMat) (u t) w x)

The full differentiated forcing pairing consists of the preceding coefficient flux and the current stream error. The principal skew flux cancels, and every spatial integrability premise is discharged.