Iterates Flow Coefficient Profile #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_sMat_small_profile_of_flow
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
(κm κprev K Cflow r₀ ρ : ℝ)
(_hK : 0 ≤ K)
(hCf : 0 ≤ Cflow)
(hr : 0 ≤ r₀)
(hρ : 0 < ρ)
(hρ1 : ρ ≤ 1)
(hflow : ∀ (t : ℝ) (l : ℤ), ContDiff ℝ (↑⊤) (I.flowGrad hΦ m l t))
(hKm : ∀ (t : ℝ) (j k : Fin 2), |I.Kmat κm m t j k| ≤ K * κprev)
(hzero :
∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ),
I.hatXiML m l t ≠ 0 → ∀ (j k : Fin 2), |(I.flowGrad hΦ m l t x - 1) j k| ≤ Cflow * ρ)
(hpositive :
∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ),
I.hatXiML m l t ≠ 0 →
∀ (p : List (Fin 2)),
1 ≤ p.length →
∀ (j k : Fin 2),
|iterateSpatialWord p (fun (y : Homogenization.Vec 2) => (I.flowGrad hΦ m l t y - 1) j k) x| ≤ Cflow * ↑p.length.factorial * r₀ ^ p.length)
(hκprev : 0 ≤ κprev)
(hκscale : |κm| ≤ κprev)
(hrad : 1 ≤ r₀ / ρ)
(t : ℝ)
(x : Homogenization.Vec 2)
(p : List (Fin 2))
(j k : Fin 2)
:
Actual coefficient jets follow from the finite cutoff average and the active flow jets. The small zeroth flow jet and positive analytic jets use the inflated radius; no sMat coefficient estimate is a premise.
theorem
AVenhance.Infra.Section4.iterate_constant_plus_small_matrix_profile
{A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ}
(hA : ContDiff ℝ (↑⊤) A)
(B : Matrix (Fin 2) (Fin 2) ℝ)
{κ Csmall Cbase ρ r : ℝ}
(hκ : 0 ≤ κ)
(_hCs : 0 ≤ Csmall)
(hCb : 0 ≤ Cbase)
(hρ : 0 ≤ ρ)
(hr : 0 ≤ r)
(hB : ∀ (j k : Fin 2), |B j k| ≤ κ * Cbase * ρ)
(hsmall :
∀ (p : List (Fin 2)) (x : Homogenization.Vec 2) (j k : Fin 2),
|iterateMatrixWord A p x j k| ≤ κ * Csmall * ρ * ↑p.length.factorial * r ^ p.length)
(p : List (Fin 2))
(x : Homogenization.Vec 2)
(j k : Fin 2)
:
Adding a spatially constant coefficient preserves the positive small jets, and its zeroth bound adds to the small sMat coefficient.