Profile

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.Profile.coarseCoeff_list_sum_bound {α : Type u_1} (L : List α) (f : α → ℝ) (C : ℝ) (h : ∀ a ∈ L, f a ≤ C) : (List.map f L).sum ≤ ↑L.length * C

theorem AVenhance.Infra.Section4.coarseCoeffWordBudget_profile {k κ A R : ℝ} (hk : 0 ≤ k) (hA : 0 ≤ A) (hR : 0 ≤ R) (w : List (Fin 2)) : coarseCoeffWordBudget k κ (fun (n : ℕ) => A * ↑n.factorial * R ^ n) w ≤ (2 * k * A + 4 * (k + |κ|) * A * (A + 1)) * ↑w.length.factorial * (2 * R) ^ w.length

Quadratic flow products preserve the factorial analytic profile, with a factor two in the radius and a constant polynomial in the small amplitude.

theorem AVenhance.Infra.Section4.CoarseCoeffForm.small_profile_of_flow {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hΦ : IsStreamSeq I Φ} {m : ℕ} {κ : ℝ} {s : ℝ → Homogenization.Vec 2 → CoarseMatrix} (hs : CoarseCoeffForm I hΦ m κ s) (hm : 1 ≤ m) {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)) (hK : ∀ (t : ℝ) (i j : Fin 2), |I.Kmat κ m t i j| ≤ k) (hzero : ∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (i j : Fin 2), |(I.flowGrad hΦ m l t x - 1) i j| ≤ Cflow * ρ) (hpositive : ∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (p : List (Fin 2)), 1 ≤ p.length → ∀ (i j : Fin 2), |iterateSpatialWord p (fun (y : Homogenization.Vec 2) => (I.flowGrad hΦ m l t y - 1) i j) x| ≤ Cflow * ↑p.length.factorial * r₀ ^ p.length) (t : ℝ) (x : Homogenization.Vec 2) (p : List (Fin 2)) (i j : Fin 2) : |iterateSpatialWord p (fun (y : Homogenization.Vec 2) => s t y i j) x| ≤ (2 * k * (Cflow * ρ) + 4 * (k + |κ|) * (Cflow * ρ) * (Cflow * ρ + 1)) * ↑p.length.factorial * (2 * max 1 (r₀ / ρ)) ^ p.length

A common small analytic coefficient profile, including the candidate. The positive flow profile is first inflated so every factor carries ρ.