The complete actual all-order stream contribution under the stream-regularity estimates.
theorem
AVenhance.Infra.Section4.iterate_increment_terminal_stream_flux_bound_of_A3
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
{κm κprev : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
(hθ : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => θprev z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(hm : 2 ≤ m)
(hκ : 0 < κprev)
(hA3 :
∀ (j : ℕ),
1 ≤ j →
∀ (t : ℝ) (n : ℕ),
2 ≤ n →
barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3)))
(hθp : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (θprev t))
{s : ℝ}
(hs0 : 0 ≤ s)
(hs1 : s ≤ 1)
(i : ℕ)
(hi : i ≤ Nstar β)
(j : Fin 2)
(w : List (Fin 2))
{B L : ℝ}
(hL : 0 < L)
(hg : 2 * (256 * (epsilon β I.Λ (m - 1))⁻¹ / L) ^ 2 ≤ 1 / 4)
(D : ℕ → ℝ)
(hfirst :
∀ (p : List (Fin 2)),
p.length = w.length →
(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p (iterateIncrement T i t))) ≤ B ^ 2 * (↑(w.length + 2 * i).factorial * L ^ w.length) ^ 2 * D w.length ^ 2)
(hhigh :
∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => decide (2 ≤ p.1.length)) (iterateSpatialSplits (j :: w)),
(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p.2 (iterateIncrement T i t))) ≤ B ^ 2 * (↑(p.2.length + 2 * i).factorial * L ^ p.2.length) ^ 2 * D p.2.length ^ 2)
:
|∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord (j :: w) (iterateIncrement T i z.1)) z.2)
(iterateWordFlux (fun (y : Homogenization.Vec 2) => Φ (m - 1) z.1 y • sigmaMat) (iterateIncrement T i z.1)
(j :: w) z.2)| ≤ (κprev / 8 * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord (j :: w) (iterateIncrement T i t))) + 2 * (2 ^ 19 * a β I.Λ (m - 1)) * B ^ 2 / L ^ 2 * (↑(w.length + 1 + 2 * i).factorial * L ^ (w.length + 1)) ^ 2 * D w.length ^ 2 + 16 / κprev * (32 * a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ 2) ^ 2 * B ^ 2 * (2 * (256 * (epsilon β I.Λ (m - 1))⁻¹ / L) ^ 2) ^ 2 * (↑(w.length + 1 + 2 * i).factorial * L ^ (w.length + 1)) ^ 2 * ∑ k ∈ Finset.range w.length, (1 / 4) ^ k * D (w.length - 1 - k) ^ 2
Combine the actual first and high stream jets; the skew principal term vanishes. Only strictly lower current scalar orders are inductive inputs.