Actual high coefficient-order flux with the quadratic norm kernel.

theorem AVenhance.Infra.Section4.iterate_terminal_analytic_high_flux_bound {s : ℝ} (hs1 : s ≤ 1) {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)) (w : List (Fin 2)) (a : ℕ) {κ C B r L : ℝ} (hκ : 0 < κ) (hL : 0 < L) (hg : 2 * (r / L) ^ 2 ≤ 1 / 4) (D : ℕ → ℝ) (hcoef : ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => decide (2 ≤ p.1.length)) (iterateSpatialSplits w), ContinuousOn (fun (z : AmnrSpace) => iterateMatrixWord (A z.1) p.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hjet : ∀ (t : ℝ) (x : Homogenization.Vec 2), ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => decide (2 ≤ p.1.length)) (iterateSpatialSplits w), ∀ (j k : Fin 2), |iterateMatrixWord (A t) p.1 x j k| ≤ κ * C * ↑p.1.length.factorial * r ^ p.1.length) (hE : ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => decide (2 ≤ p.1.length)) (iterateSpatialSplits w), (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p.2 (v t))) ≤ B ^ 2 * (↑(p.2.length + a).factorial * L ^ p.2.length) ^ 2 * D p.2.length ^ 2) : |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u z.1)) z.2) (iterateSplitFlux (List.filter (fun (p : List (Fin 2) × List (Fin 2)) => decide (2 ≤ p.1.length)) (iterateSpatialSplits w)) (A z.1) (v z.1) z.2)| ≤ (κ / 8 * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (u t))) + 16 * κ * C ^ 2 * B ^ 2 * (2 * (r / L) ^ 2) ^ 2 * (↑(w.length + a).factorial * L ^ w.length) ^ 2 * ∑ k ∈ Finset.range (w.length - 1), (1 / 4) ^ k * D (w.length - 2 - k) ^ 2

Analytic high coefficient jets and lower scalar energies bound the actual high-order flux. All scalar premises have word length at most n-2.