Locally finite sums of all actual mixed stream jets.
theorem
AVenhance.Infra.Section4.amnr_streamIncrement_word_sum
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
(w : List (Option (Fin 2)))
(z : AmnrSpace)
:
∃ (s : Finset ℤ),
s.card ≤ 3 ∧ amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) w
(fun (y : AmnrSpace) => Φ m y.1 y.2 - Φ (m - 1) y.1 y.2) z = ∑ k ∈ s,
amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) w
(fun (y : AmnrSpace) => I.nextStreamTerm m (Φ (m - 1)) ⋯ y.1 y.2 k) z
Every actual stream differential word is a sum of at most three terms.
theorem
AVenhance.Infra.Section4.amnr_streamIncrement_mixed_abs_le_of_A3
{β C : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(hreg : StreamRegularityBounds C I Φ)
{m : ℕ}
(hm : 1 ≤ m)
(α : List (Fin 2))
(ℓ : ℕ)
(hbudget : α.length + 2 * ℓ ≤ Nstar β)
(z : AmnrSpace)
:
|amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α ++ List.replicate ℓ none)
(fun (y : AmnrSpace) => Φ m y.1 y.2 - Φ (m - 1) y.1 y.2) z| ≤ 3 * (2 ^ ℓ * I.Chat * I.Czeta * (amnrTransportSpatialConstant (Nstar β) * a β I.Λ m * epsilon β I.Λ m ^ 2 * (epsilon β I.Λ m)⁻¹ ^ α.length) * (tau β I.Λ m)⁻¹ ^ ℓ)
Full source mixed stream-increment estimate from the actual three-term local sum. No mixed derivative estimate is assumed.