Iterates Actual First Forcing Pairing #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_actual_first_forcing_pairing_bound
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(hNstar : 1 ≤ Nstar β)
{m : ℕ}
{κm κ : ℝ}
(hm : 1 ≤ m)
(hκm : 0 < κm)
(hκ : 0 < κ)
{u : ℝ → Homogenization.Vec 2 → ℝ}
{u₀ : Homogenization.Vec 2 → ℝ}
(hsol : IsClassicalSol (streamVel (Φ (m - 1))) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) u₀ u)
(hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(w : List (Fin 2))
(hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2)
{B N r L C Ccoef D ρ q s : ℝ}
(hB : 0 ≤ B)
(hN : 0 ≤ N)
(hr : 0 ≤ r)
(hC : 0 ≤ C)
(hD : 0 ≤ D)
(hq : 0 < q)
(hρ : 0 ≤ ρ)
(hρq : ρ ≤ q)
(hL : 0 < L)
(hs : 0 ≤ s)
(hs1 : s ≤ 1)
(hg : 2 * (r / L) ^ 2 ≤ 1 / 2)
(hscale : B * r ≤ C * κ * L ^ 2)
(hQb : ∀ (t : ℝ) (j k : Fin 2), |iterateKmatPrimitive I κm m t j k| ≤ D)
(hQscale : D * L ^ 2 ≤ C * q)
(hjet :
∀ (j k : Fin 2) (t : ℝ) (x : Homogenization.Vec 2),
∀
p ∈
List.filter (fun (p : List (Fin 2) × List (Fin 2)) => decide (1 ≤ p.1.length))
(iterateSpatialSplits (j :: k :: w)),
∀ (a : Fin 2),
|iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => streamVel (Φ (m - 1)) t y a) x| ≤ B * ↑p.1.length.factorial * r ^ p.1.length)
(hE :
∀ (v : List (Fin 2)),
v.length ≤ w.length + 3 →
(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord v (u t))) ≤ (N / √κ) ^ 2 * (↑v.length.factorial * L ^ v.length) ^ 2)
(hcoef :
∀ (t : ℝ) (x : Homogenization.Vec 2) (v : List (Fin 2)) (j k : Fin 2),
|iterateMatrixWord (fun (y : Homogenization.Vec 2) => timeAvgMat (I.Kmat κm m) - κ • 1 + I.sMat hΦ m κm t y) v x j
k| ≤ κ * (Ccoef * ρ) * ↑v.length.factorial * r ^ v.length)
(hTE :
∀ (j k : Fin 2),
l2NormSq (iterateSpatialWord (j :: k :: w) (u s)) ≤ (N * ↑(w.length + 2).factorial * L ^ (w.length + 2)) ^ 2)
:
|∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (I.TForcing hΦ m κm κ u z.1)) z.2)
((iterateKmatPrimitive I κm m z.1).mulVec (spaceGrad (iterateSpatialWord w (u z.1)) z.2))| ≤ ((8 + 32 * √(8 + 64 * C ^ 2)) * C ^ 2 + 1 + 128 * C ^ 2 * Ccoef ^ 2) * q ^ 2 * (N * ↑(w.length + 2).factorial * L ^ w.length) ^ 2