Summation of new lattice shells along monotone real cutoffs, with the strict cutoff boundaries expressed through ceiling and half-open integer intervals.

theorem KamProject.Arnold1963.Iteration.shell_sum_telescope (N : ℕ → ℝ) (hN : Monotone N) (s : ℕ) : ∑ j ∈ Finset.range s, newShellBudget (N j) (N (j + 1)) = newShellBudget (N 0) (N s)

theorem KamProject.Arnold1963.Iteration.shell_budget_one_le_two (N : ℝ) : newShellBudget 1 N ≤ 2

theorem KamProject.Arnold1963.Iteration.shell_summable (N : ℕ → ℝ) (hN : Monotone N) (h0 : N 0 = 1) : Summable fun (s : ℕ) => newShellBudget (N s) (N (s + 1))

theorem KamProject.Arnold1963.Iteration.shell_tsum_le_two (N : ℕ → ℝ) (hN : Monotone N) (h0 : N 0 = 1) : ∑' (s : ℕ), newShellBudget (N s) (N (s + 1)) ≤ 2