Iterates Terminal Flow Scale

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_terminal_flow_pairings_bound_of_previous_energy {s : ℝ} (hs1 : s ≤ 1) {flow a b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} {κ D B C ρ E : ℝ} (hκ : 0 < κ) (hC : 0 ≤ C) (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) (hscale : D * B ≤ C * κ * ρ) (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) (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