Bounds for the surviving grades of the actual finite packet residual.

theorem EulerPacketTailBound.sum_geometric_le_two (q : ℝ) (hq : 0 ≤ q) (hqhalf : q ≤ 1 / 2) (N : ℕ) : ∑ i ∈ Finset.range N, q ^ i ≤ 2

theorem EulerPacketTailBound.sum_geometric_Ico_le (q : ℝ) (hq : 0 ≤ q) (hqhalf : q ≤ 1 / 2) (a b : ℕ) : ∑ i ∈ Finset.Ico a b, q ^ i ≤ 2 * q ^ a

theorem EulerPacketTailBound.finite_tail_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (κ B : ℝ) (hκ : 0 ≤ κ) (hB : 0 ≤ B) (hsmall : κ * B ≤ 1 / 2) (N : ℕ) (c : ℕ → E) (hc : ∀ n ∈ Finset.Ico (N + 1) (2 * N + 3), ‖c n‖ ≤ B ^ (n + 1)) : ‖∑ n ∈ Finset.Ico (N + 1) (2 * N + 3), κ ^ n • c n‖ ≤ 2 * B * (κ * B) ^ (N + 1)

theorem EulerPacketTailBound.normalized_tail_norm_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k B C : ℝ) (hk : 0 ≤ k) (hB : 0 ≤ B) (hsmall : B / k ≤ 1 / 2) (L : E →L[ℝ] F) (hL : ‖L‖ ≤ C) (N : ℕ) (c : ℕ → E) (hc : ∀ n ∈ Finset.Ico (N + 1) (2 * N + 3), ‖c n‖ ≤ B ^ (n + 1)) : ‖k • L (∑ n ∈ Finset.Ico (N + 1) (2 * N + 3), k⁻¹ ^ n • c n)‖ ≤ 2 * C * k * B * (B / k) ^ (N + 1)

Includes the source's final k times inverse-frame normalization.