Spatial Words #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterateSpatialWord_const_mul
{f : Homogenization.Vec 2 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(c : ℝ)
(w : List (Fin 2))
:
(iterateSpatialWord w fun (x : Homogenization.Vec 2) => c * f x) = fun (x : Homogenization.Vec 2) =>
c * iterateSpatialWord w f x
A spatially constant factor commutes with every ordered derivative.
theorem
AVenhance.Infra.Section4.coarseCoeff_word_add
{f g : Homogenization.Vec 2 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(hg : ContDiff ℝ (↑⊤) g)
(w : List (Fin 2))
:
(iterateSpatialWord w fun (x : Homogenization.Vec 2) => f x + g x) = fun (x : Homogenization.Vec 2) =>
iterateSpatialWord w f x + iterateSpatialWord w g x
theorem
AVenhance.Infra.Section4.coarseCoeffWindow_word_formula
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
(κ a b t : ℝ)
(hflow : ∀ (l : ℤ), ContDiff ℝ (↑⊤) (I.flowGrad hΦ m l t))
(w : List (Fin 2))
(x : Homogenization.Vec 2)
(i j : Fin 2)
:
iterateSpatialWord w (fun (y : Homogenization.Vec 2) => coarseCoeffWindow I hΦ m κ a b t y i j) x = ∑' (l : ℤ), I.hatXiML m l t * iterateSpatialWord w
(fun (y : Homogenization.Vec 2) => coarseCoeffPolynomial a b κ (I.Kmat κ m t) (I.flowGrad hΦ m l t y) i j) x
Ordered jets of either polynomial specialization: only the spatial kernel is differentiated, never K or the time cutoff.
theorem
AVenhance.Infra.Section4.coarseCoeffWindow_word_entry_bound
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
(κ a b t : ℝ)
(hflow : ∀ (l : ℤ), ContDiff ℝ (↑⊤) (I.flowGrad hΦ m l t))
(w : List (Fin 2))
(x : Homogenization.Vec 2)
{C : ℝ}
(hG :
∀ (l : ℤ),
I.hatXiML m l t ≠ 0 →
∀ (i j : Fin 2),
|iterateSpatialWord w
(fun (y : Homogenization.Vec 2) => coarseCoeffPolynomial a b κ (I.Kmat κ m t) (I.flowGrad hΦ m l t y) i j)
x| ≤ C)
(i j : Fin 2)
:
|iterateSpatialWord w (fun (y : Homogenization.Vec 2) => coarseCoeffWindow I hΦ m κ a b t y i j) x| ≤ C
Word bounds transfer from active polynomial kernels to their convex average.