Iterates Actual All Word Stream #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_increment_terminal_all_word_stream_recurrence_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θ : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => θprev z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(hm : 2 ≤ m)
(hκ : 0 < κprev)
(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)))
(hθp : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (θprev t))
{s : ℝ}
(hs0 : 0 ≤ s)
(hs1 : s ≤ 1)
(i : ℕ)
(hi : i ≤ Nstar β)
(w : List (Fin 2))
{B L : ℝ}
(hL : 0 < L)
(hg : 2 * (256 * (epsilon β I.Λ (m - 1))⁻¹ / L) ^ 2 ≤ 1 / 4)
(D : ℕ → ℝ)
(hlower :
∀ (p : List (Fin 2)),
p.length < w.length →
(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p (iterateIncrement T i t))) ≤ B ^ 2 * (↑(p.length + 2 * i).factorial * L ^ p.length) ^ 2 * D p.length ^ 2)
:
|∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (iterateIncrement T i z.1)) z.2)
(iterateWordFlux (fun (y : Homogenization.Vec 2) => Φ (m - 1) z.1 y • sigmaMat) (iterateIncrement T i z.1) w
z.2)| ≤ ((κprev / 8 * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (iterateIncrement T i t))) + 2 * (2 ^ 19 * a β I.Λ (m - 1)) * B ^ 2 / L ^ 2 * (↑(w.length + 2 * i).factorial * L ^ w.length) ^ 2 * if w = [] then 0 else D (w.length - 1) ^ 2) + 16 / κprev * (32 * a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ 2) ^ 2 * B ^ 2 * (2 * (256 * (epsilon β I.Λ (m - 1))⁻¹ / L) ^ 2) ^ 2 * (↑(w.length + 2 * i).factorial * L ^ w.length) ^ 2 * ∑ k ∈ Finset.range (w.length - 1), (1 / 4) ^ k * D (w.length - 2 - k) ^ 2
The complete current-stream recurrence uses strictly lower coordinate-word orders and includes the vanishing order-zero contribution.