A finite packet sum keeps its first two grades separate from the geometric tail.

theorem EulerPacketCylinderField.weighted_low_high_sum_le (N : ℕ) (hN : 1 ≤ N) (κ B C₁ C₂ : ℝ) (hκ : 0 ≤ κ) (hB : 0 ≤ B) (hsmall : κ * B ≤ 1 / 2) (A : ℕ → ℝ) (hzero : A 0 = 0) (hone : A 1 ≤ C₁) (htwo : A 2 ≤ C₂) (htail : ∀ (n : ℕ), 3 ≤ n → n ≤ N + 1 → A n ≤ B ^ (n + 1)) : ∑ n ∈ Finset.range (N + 2), κ ^ n * A n ≤ κ * C₁ + κ ^ 2 * C₂ + 2 * B * (κ * B) ^ 3

def EulerPacketCylinderField.lowHighEnvelope (B C₁ C₂ : ℝ) (n : ℕ) : ℝ

Low high envelope, with branches according to n=0.

Equations

• EulerPacketCylinderField.lowHighEnvelope B C₁ C₂ n = if n = 0 then 0 else if n = 1 then C₁ else if n = 2 then C₂ else B ^ (n + 1)

theorem EulerPacketCylinderField.Field.wordBound_evaluateFamily {P T : ℝ} [Fact (0 < P)] (M : ℕ) (κ : ℝ) (f : ℕ → EulerPacketProfileRecursion.VectorField) (G : (i : ℕ) → Field P T (f i)) (q : ℕ) (R : ℝ) (A : ℕ → ℝ) (d : ℕ) (hκ : 0 ≤ κ) (hG : ∀ i ∈ Finset.range (M + 1), (G i).WordBound q R (A i) d) : (evaluateFamily M κ f G).WordBound q R (∑ i ∈ Finset.range (M + 1), κ ^ i * A i) d

theorem EulerPacketCylinderField.Field.wordBound_evaluate_low_high {P T : ℝ} [Fact (0 < P)] (N : ℕ) (hN : 1 ≤ N) (κ B C₁ C₂ : ℝ) (hκ : 0 ≤ κ) (hB : 0 ≤ B) (hsmall : κ * B ≤ 1 / 2) (f : ℕ → EulerPacketProfileRecursion.VectorField) (G : (i : ℕ) → Field P T (f i)) (q : ℕ) (R : ℝ) (hR : 0 ≤ R) (hzero : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), f 0 (↑t, x, θ) = 0) (hone : (G 1).WordBound q R C₁ 0) (htwo : (G 2).WordBound q R C₂ 0) (htail : ∀ (n : ℕ), 3 ≤ n → n ≤ N + 1 → (G n).WordBound q R (B ^ (n + 1)) 0) : (evaluateFamily (N + 1) κ f G).WordBound q R (κ * C₁ + κ ^ 2 * C₂ + 2 * B * (κ * B) ^ 3) 0