Iterates Terminal Transpose Pairing

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_terminal_transpose_pairing_bound_of_continuity {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} {a b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {σ D s : ℝ} (hs1 : s ≤ 1) (hσ : 0 < σ) (ha : ContinuousOn (fun (z : AmnrSpace) => a z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hb : ContinuousOn (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hQc : ContinuousOn (fun (z : AmnrSpace) => Q z.1) (Set.Ici 0 ×ˢ Set.univ)) (hQ : ∀ (t : ℝ) (j k : Fin 2), |Q t j k| ≤ D) : |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (a z.1 z.2) ((Q z.1).mulVec (b z.1 z.2))| ≤ σ * spaceTimeGradNormSq b + D ^ 2 / σ * spaceTimeGradNormSq a

Reverse the matrix pairing before Young allocation, preserving the desired scalar dissipation factor and proving natural integrability.