Actual increment material-gradient energy from forcing and velocity bounds.
theorem
AVenhance.Infra.Section4.iterate_increment_material_gradient_energy_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θ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hm : 2 ≤ m)
(hκm : 0 < κm)
(hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2)
(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)))
(i : ℕ)
(hi : i + 1 ≤ Nstar β)
(w : List (Fin 2))
{C Gcur Gprev r L : ℝ}
(hL : 0 < L)
(hg : 2 * (r / L) ^ 2 ≤ 1 / 2)
(hvel : 2 * (256 * (epsilon β I.Λ (m - 1))⁻¹ / L) ^ 2 ≤ 1 / 2)
(hcoef :
∀ (t : ℝ) (x : Homogenization.Vec 2) (q : 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) q x j k| ≤ κprev * C * ↑q.length.factorial * r ^ q.length)
(hcur :
∀ (q : List (Fin 2)),
q.length ≤ w.length + 2 →
(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord q (iterateIncrement T (i + 1) t))) ≤ Gcur ^ 2 * (↑(q.length + 2 * (i + 1)).factorial * L ^ q.length) ^ 2)
(hprev :
∀ (q : List (Fin 2)),
q.length ≤ w.length + 2 →
(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord q (iterateIncrement T i t))) ≤ Gprev ^ 2 * (↑(q.length + 2 * i).factorial * L ^ q.length) ^ 2)
:
(spaceTimeGradNormSq fun (t : ℝ) =>
spaceGrad
(amnrMaterial (streamVel (Φ (m - 1))) (fun (s : ℝ) => iterateSpatialWord w (iterateIncrement T (i + 1) s)) t)) ≤ 8 * κprev ^ 2 * Gcur ^ 2 * (↑(w.length + 2 + 2 * (i + 1)).factorial * L ^ (w.length + 2)) ^ 2 + 512 * κprev ^ 2 * C ^ 2 * Gprev ^ 2 * (↑(w.length + 2 + 2 * i).factorial * L ^ (w.length + 2)) ^ 2 + 544 * (8192 * a β I.Λ (m - 1) * epsilon β I.Λ (m - 1)) ^ 2 * (256 * (epsilon β I.Λ (m - 1))⁻¹) ^ 2 * Gcur ^ 2 * (↑(w.length + 1 + 2 * (i + 1)).factorial * L ^ w.length) ^ 2
The previous-increment material estimate follows from its actual PDE, analytic coefficient jets, the stream-regularity estimates, and the two preceding scalar energies. No material or differentiated forcing bound is supplied as a premise.