Word Bounds

Support for the Armstrong–Vicol anomalous-diffusion formalization.

def AVenhance.Infra.Section4.coarseCoeffWordBudget (K κ : ℝ) (F : ℕ → ℝ) (w : List (Fin 2)) : ℝ

Every ordered split is retained, including repetitions. The only added factor is the undifferentiated identity in the right Jacobian F = (F-I)+I.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section4.WordBounds.list_abs_sum_bound {α : Type u_1} (L : List α) (f g : α → ℝ) (h : ∀ a ∈ L, |f a| ≤ g a) : |(List.map f L).sum| ≤ (List.map g L).sum

theorem AVenhance.Infra.Section4.coarseCoeff_constant_matrix_word {D : Homogenization.Vec 2 → CoarseMatrix} (hD : ContDiff ℝ (↑⊤) D) (K : CoarseMatrix) (w : List (Fin 2)) (x : Homogenization.Vec 2) (i j : Fin 2) : iterateSpatialWord w (fun (y : Homogenization.Vec 2) => (K * D y) i j) x = ∑ p : Fin 2, K i p * iterateSpatialWord w (fun (y : Homogenization.Vec 2) => D y p j) x

theorem AVenhance.Infra.Section4.coarseCoeff_quadratic_word {D F : Homogenization.Vec 2 → CoarseMatrix} (hD : ContDiff ℝ (↑⊤) D) (hF : ContDiff ℝ (↑⊤) F) (C : CoarseMatrix) (w : List (Fin 2)) (x : Homogenization.Vec 2) (i j : Fin 2) : iterateSpatialWord w (fun (y : Homogenization.Vec 2) => (Matrix.transpose (D y) * C * F y) i j) x = ∑ q : Fin 2, ∑ p : Fin 2, C p q * (List.map (fun (r : List (Fin 2) × List (Fin 2)) => iterateSpatialWord r.1 (fun (y : Homogenization.Vec 2) => D y p i) x * iterateSpatialWord r.2 (fun (y : Homogenization.Vec 2) => F y q j) x) (iterateSpatialSplits w)).sum

The quadratic term is an explicit Leibniz expansion of two flow factors.

theorem AVenhance.Infra.Section4.coarseCoeffPolynomial_word_entry_bound {F : Homogenization.Vec 2 → CoarseMatrix} (hF : ContDiff ℝ (↑⊤) F) {K : CoarseMatrix} {k a b κ : ℝ} {B : ℕ → ℝ} (ha : |a| ≤ 1) (hb : |b| ≤ 1) (hB : ∀ (n : ℕ), 0 ≤ B n) (hK : ∀ (i j : Fin 2), |K i j| ≤ k) (hjets : ∀ (w : List (Fin 2)) (x : Homogenization.Vec 2) (i j : Fin 2), |iterateSpatialWord w (fun (y : Homogenization.Vec 2) => (F y - 1) i j) x| ≤ B w.length) (w : List (Fin 2)) (x : Homogenization.Vec 2) (i j : Fin 2) : |iterateSpatialWord w (fun (y : Homogenization.Vec 2) => coarseCoeffPolynomial a b κ K (F y) i j) x| ≤ coarseCoeffWordBudget k κ B w

Quantitative jets of the polynomial use only actual flow jets, at all suborders in the ordered Leibniz rule. No coefficient jet is assumed.

theorem AVenhance.Infra.Section4.CoarseCoeffForm.word_entry_bound {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hΦ : IsStreamSeq I Φ} {m : ℕ} {κ : ℝ} {s : ℝ → Homogenization.Vec 2 → CoarseMatrix} (hs : CoarseCoeffForm I hΦ m κ s) (hm : 1 ≤ m) (t : ℝ) {k : ℝ} {B : ℕ → ℝ} (hB : ∀ (n : ℕ), 0 ≤ B n) (hK : ∀ (i j : Fin 2), |I.Kmat κ m t i j| ≤ k) (hflow : ∀ (l : ℤ), ContDiff ℝ (↑⊤) (I.flowGrad hΦ m l t)) (hjets : ∀ (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (v : List (Fin 2)) (y : Homogenization.Vec 2) (i j : Fin 2), |iterateSpatialWord v (fun (z : Homogenization.Vec 2) => (I.flowGrad hΦ m l t z - 1) i j) y| ≤ B v.length) (w : List (Fin 2)) (x : Homogenization.Vec 2) (i j : Fin 2) : |iterateSpatialWord w (fun (y : Homogenization.Vec 2) => s t y i j) x| ≤ coarseCoeffWordBudget k κ B w

The full coefficient jet budget is derived from the active flow jets. This applies unchanged to the old and left-Jacobian instances.