Iterates Terminal Flow Pairing

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_terminal_flow_commutator_pairings_bound {s : ℝ} (hs1 : s ≤ 1) {flow a b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} {κ D B : ℝ} (hκ : 0 < κ) (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) (ha : MeasureTheory.IntegrableOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecNormSq (a p.1 p.2)) timeCube MeasureTheory.volume) (hb : MeasureTheory.IntegrableOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecNormSq (b p.1 p.2)) timeCube MeasureTheory.volume) (hp₁ : MeasureTheory.IntegrableOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (a p.1 p.2) ((Q p.1).mulVec ((gradMatrix (flow p.1) p.2).mulVec (b p.1 p.2)))) timeCube MeasureTheory.volume) (hp₂ : MeasureTheory.IntegrableOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot ((gradMatrix (flow p.1) p.2).mulVec (a p.1 p.2)) ((Q p.1).mulVec (b p.1 p.2))) timeCube MeasureTheory.volume) : |∫ (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 * D ^ 2 * B ^ 2 / κ * spaceTimeGradNormSq b