Iterates Terminal Flow Regularity

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_terminal_flow_pairings_bound_of_continuity {flow a b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} {κ D B C ρ E s : ℝ} (hs1 : s ≤ 1) (hκ : 0 < κ) (hC : 0 ≤ C) (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)) (hGc : ContinuousOn (fun (z : AmnrSpace) => gradMatrix (flow z.1) z.2) (Set.Ici 0 ×ˢ Set.univ)) (hQ : ∀ (t : ℝ) (i j : Fin 2), |Q t i j| ≤ D) (hG : ∀ (t : ℝ) (x : Homogenization.Vec 2) (i j : Fin 2), |gradMatrix (flow t) x i j| ≤ B) (hscale : D * B ≤ C * κ * ρ) (hprevious : κ * spaceTimeGradNormSq b ≤ E) : |∫ (p : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (a p.1 p.2) ((Q p.1).mulVec ((gradMatrix (flow p.1) p.2).mulVec (b p.1 p.2)))| + |∫ (p : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot ((gradMatrix (flow p.1) p.2).mulVec (a p.1 p.2)) ((Q p.1).mulVec (b p.1 p.2))| ≤ κ / 24 * spaceTimeGradNormSq a + 384 * C ^ 2 * ρ ^ 2 * E

Actual continuous flow and gradient carriers discharge every natural integrability premise in the two terminal flow commutator pairings.