Actual current increment with the corrected material budget.
theorem
AVenhance.Infra.Section4.iterate_increment_terminal_current_material_corrected_bound
{β : ℝ}
(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θ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hm : 1 ≤ m)
(hκm : 0 < κm)
(hκ : 0 < κprev)
(hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2)
{s : ℝ}
(hs1 : s ≤ 1)
(i : ℕ)
(hi : i + 1 ≤ Nstar β)
(w : List (Fin 2))
{Ccoef Cscale B r L D q : ℝ}
(hL : 0 < L)
(hg : 2 * (r / L) ^ 2 ≤ 1 / 2)
(hD : 0 ≤ D)
(hCscale : 0 ≤ Cscale)
(hq : 0 < q)
{Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ}
(hQc : ContinuousOn Q (Set.Ici 0))
(hQ : ∀ (t : ℝ) (j k : Fin 2), |Q t j k| ≤ D)
(hscale : D * L ^ 2 ≤ Cscale * q)
(hcoef :
∀ (t : ℝ) (x : Homogenization.Vec 2) (p : List (Fin 2)) (j k : Fin 2),
|iterateMatrixWord (fun (y : Homogenization.Vec 2) => I.Kmat κm m t - κprev • 1 + I.sMat hΦ m κm t y) p x j k| ≤ κprev * Ccoef * ↑p.length.factorial * r ^ p.length)
(hprev :
∀ (p : List (Fin 2)),
p.length ≤ w.length + 2 →
(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p (iterateIncrement T i t))) ≤ B ^ 2 * (↑(p.length + 2 * i).factorial * L ^ p.length) ^ 2)
:
|∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot
(spaceGrad (iterateSpatialWord w (amnrMaterial (streamVel (Φ (m - 1))) (iterateIncrement T (i + 1)) z.1)) z.2)
((Q z.1).mulVec (spaceGrad (iterateSpatialWord w (iterateIncrement T i z.1)) z.2))| ≤ (κprev / 24 * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (iterateIncrement T (i + 1) t))) + (24 * Cscale ^ 2 * q ^ 2 + (1 + Cscale ^ 2 * (32 * Ccoef ^ 2)) * q) * (4 * κprev * B ^ 2 * (↑(w.length + 2 + 2 * i).factorial * L ^ w.length) ^ 2)
Derive the linear and quadratic oscillatory remainder from actual forcing jets and the preceding increment energies.