High stream forcing for the actual finite increments under the stream-regularity estimates.
theorem
AVenhance.Infra.Section4.iterate_increment_terminal_high_stream_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)))
{s : ℝ}
(hs1 : s ≤ 1)
(i : ℕ)
(hi : i ≤ Nstar β)
(w : List (Fin 2))
{B L : ℝ}
(hL : 0 < L)
(hg : 2 * (256 * (epsilon β I.Λ (m - 1))⁻¹ / L) ^ 2 ≤ 1 / 4)
(D : ℕ → ℝ)
(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 (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 w (iterateIncrement T i z.1)) z.2)
(iterateSplitFlux
(List.filter (fun (p : List (Fin 2) × List (Fin 2)) => decide (2 ≤ p.1.length)) (iterateSpatialSplits w))
(fun (y : Homogenization.Vec 2) => Φ (m - 1) z.1 y • sigmaMat) (iterateIncrement T i z.1) z.2)| ≤ (κprev / 8 * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (iterateIncrement T i t))) + 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 + 2 * i).factorial * L ^ w.length) ^ 2 * ∑ k ∈ Finset.range (w.length - 1), (1 / 4) ^ k * D (w.length - 2 - k) ^ 2
The stream-regularity estimates control the actual high stream-jet part of the increment energy recurrence. All scalar bounds are at least two orders below w.