Representation #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.coarseCoeffWindow_eq_sum
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
(κ a b t : ℝ)
(x : Homogenization.Vec 2)
:
coarseCoeffWindow I hΦ m κ a b t x = ∑ l ∈ ⋯.toFinset, I.hatXiML m l t • coarseCoeffPolynomial a b κ (I.Kmat κ m t) (I.flowGrad hΦ m l t x)
Finite window representation, valid for either polynomial specialization.
theorem
AVenhance.Infra.Section4.coarseCoeffWindow_eq_tsum
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
(κ a b t : ℝ)
(x : Homogenization.Vec 2)
:
coarseCoeffWindow I hΦ m κ a b t x = ∑' (l : ℤ), I.hatXiML m l t • coarseCoeffPolynomial a b κ (I.Kmat κ m t) (I.flowGrad hΦ m l t x)
A single tsum of a matrix polynomial: the structural form from the plan.
theorem
AVenhance.Infra.Section4.CoarseCoeffForm.periodic
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{hΦ : IsStreamSeq I Φ}
{m : ℕ}
{κ : ℝ}
{s : ℝ → Homogenization.Vec 2 → CoarseMatrix}
(hs : CoarseCoeffForm I hΦ m κ s)
(t : ℝ)
(hp : ∀ (l : ℤ), IsZ2Periodic (I.flowGrad hΦ m l t))
:
IsZ2Periodic (s t)