Iterates Actual Mean Correction Energy #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_actual_mean_correction_energy_bound
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
{κm κ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)
{u : ℝ → Homogenization.Vec 2 → ℝ}
(hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(w : List (Fin 2))
{N C ρ r L : ℝ}
(hL : 0 < L)
(hg : 2 * (r / L) ^ 2 ≤ 1 / 2)
(hD :
∀ (t : ℝ) (x : Homogenization.Vec 2) (v : List (Fin 2)) (j k : Fin 2),
|iterateMatrixWord (fun (y : Homogenization.Vec 2) => timeAvgMat (I.Kmat κm m) - κprev • 1 + I.sMat hΦ m κm t y) v x
j k| ≤ κprev * (C * ρ) * ↑v.length.factorial * r ^ v.length)
(hE :
∀ (v : List (Fin 2)),
v.length ≤ w.length + 2 →
(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord v (u t))) ≤ (N / √κprev) ^ 2 * (↑v.length.factorial * L ^ v.length) ^ 2)
:
The noncentered first-step forcing remainder has a squared smallness energy gain from actual mean/spatial coefficient jets and scalar bounds.