Actual all-order material forcing energy for the increments.
theorem
AVenhance.Infra.Section4.iterate_increment_analytic_TForcing_energy_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θ : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => θprev z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(hm : 1 ≤ m)
(hκm : 0 < κm)
(hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2)
(i : ℕ)
(hi : i ≤ Nstar β)
(w : List (Fin 2))
(a : ℕ)
{κ C B b L : ℝ}
(hL : 0 < L)
(hg : 2 * (b / L) ^ 2 ≤ 1 / 2)
(hD :
∀ (t : ℝ) (x : Homogenization.Vec 2) (r : 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) r x j k| ≤ κ * C * ↑r.length.factorial * b ^ r.length)
(hE :
∀ (r : List (Fin 2)),
r.length ≤ w.length + 2 →
(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord r (iterateIncrement T i t))) ≤ B ^ 2 * (↑(r.length + a).factorial * L ^ r.length) ^ 2)
:
The actual differentiated TForcing gradient is bounded by preceding increment energies and actual coefficient jets. Natural integrability and regularity are discharged from the scalar carrier and flow smoothness.