Natural integrability for every terminal selected coefficient flux.

theorem AVenhance.Infra.Section4.iterate_truncated_flux_pairing_bound_of_continuous_jets {s : ℝ} (hs1 : s ≤ 1) (P : List (List (Fin 2) × List (Fin 2))) {A : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hA : ∀ p ∈ P, ContinuousOn (fun (z : AmnrSpace) => iterateMatrixWord (A z.1) p.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (ρ D : List (Fin 2) × List (Fin 2) → ℝ) (hρ : ∀ p ∈ P, 0 < ρ p) (hAj : ∀ (t : ℝ) (x : Homogenization.Vec 2), ∀ p ∈ P, ∀ (i j : Fin 2), |iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => A t y i j) x| ≤ D p) : |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u z.1)) z.2) (iterateSplitFlux P (A z.1) (v z.1) z.2)| ≤ ((List.map ρ P).sum * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (u t))) + (List.map (fun (p : List (Fin 2) × List (Fin 2)) => D p ^ 2 / ρ p * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p.2 (v t))) P).sum

All-order space-time forcing estimate with natural integrability discharged from actual scalar smoothness and conditional coefficient continuity.