The first stream radius gain for the actual selected vector flux.

theorem AVenhance.Infra.Section4.iterate_truncated_first_stream_flux_analytic_bound {φ u : ℝ → Homogenization.Vec 2 → ℝ} {H B L d : ℝ} (hH : 0 < H) (hL : 0 < L) (hφ : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => φ z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) {s : ℝ} (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (hφp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (φ t)) (hup : ∀ (t : ℝ), 0 < t → IsZ2Periodic (u t)) (j : Fin 2) (w : List (Fin 2)) (i : ℕ) (hjet : ∀ (t : ℝ) (x : Homogenization.Vec 2) (j k : Fin 2), |spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad (φ t) y j) x k| ≤ H) (hM : ∀ (q : List (Fin 2)), q.length = w.length → (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord q (u t))) ≤ B ^ 2 * (↑(w.length + 2 * i).factorial * L ^ w.length) ^ 2 * d ^ 2) : |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord (j :: w) (u z.1)) z.2) (iterateSplitFlux (List.filter (fun (p : List (Fin 2) × List (Fin 2)) => p.1.length == 1) (iterateSpatialSplits (j :: w))) (fun (y : Homogenization.Vec 2) => φ z.1 y • sigmaMat) (u z.1) z.2)| ≤ 2 * H * B ^ 2 / L ^ 2 * (↑(w.length + 1 + 2 * i).factorial * L ^ (w.length + 1)) ^ 2 * d ^ 2

Exact first-order multiplicity and radius gain in the energy's actual flux.