Natural integrability for the current oscillatory material pairing.

theorem AVenhance.Infra.Section4.iterate_truncated_current_word_material_pairing_bound_of_continuity {s : ℝ} (hs1 : s ≤ 1) {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ D σ : ℝ} {F u v : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} (hsol : IsClassicalSol b κ F u₀ u) (w : List (Fin 2)) (hκ : 0 < κ) (hσ : 0 < σ) (hQ : ∀ (t : ℝ) (i j : Fin 2), |Q t i j| ≤ D) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hvp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (v t)) (hF : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (F t)) (hFc : ContinuousOn (fun (z : AmnrSpace) => spaceGrad (iterateSpatialWord w (F z.1)) z.2) (Set.Ici 0 ×ˢ Set.univ)) (hQc : ContinuousOn Q (Set.Ici 0)) : |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (amnrMaterial b u z.1)) z.2) ((Q z.1).mulVec (spaceGrad (v z.1) z.2))| ≤ (((κ / 24 * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (u t))) + 24 * κ * D ^ 2 * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2) => spaceLap (fun (y : Homogenization.Vec 2) => spaceGrad (v t) y j) x) + σ * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (v t)) + D ^ 2 / σ * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (F t))

The current material budget requires no separately assumed integrability of diffusion or forcing pairings. Actual smoothness supplies them.