Partial sums

Stream: Is there code for X?

[Niels Voss]

Is there a way to sum over nat? I have defined

/--
`partial_sum f n` is the sum `f 0 + f 1 + f 2 + ... + f (n - 1)`. Note that this does not include
the term `f n`.
-/
def partial_sum {R : Type u} [add_comm_monoid R] (f : ℕ → R) (n : ℕ) :=
∑ i in finset.range n, f i

but I wonder if this definition already exists in mathlib (perhaps it could be generalized to locally_finite_order_bot). Even if this is not worth defining, are there any lemmas about ∑ i in finset.range n, f i? I'm currently trying to prove the Riemann Series Theorem, which cannot be expressed using tsum.

[Yury G. Kudryashov]

We just use ∑ i in finset.range n, f i

[Yury G. Kudryashov]

What kind of lemmas do you want?

[Yury G. Kudryashov]

Which proof are you formalizing? Does it imply that the set of sums of rearrangements is an affine subspsace?

[Niels Voss]

I just needed a couple short ones, like these:

lemma partial_sum_next {R : Type u} [add_comm_monoid R] (f : ℕ → R) (n : ℕ) :
  partial_sum f (n + 1) = f n + partial_sum f n :=
begin
  unfold partial_sum,
  rw finset.range_succ,
  apply finset.sum_insert,
  exact finset.not_mem_range_self
end

lemma partial_sum_neg {R : Type u} [add_comm_group R] (f : ℕ → R) (n : ℕ) :
  partial_sum (λ m, - (f m)) n = - (partial_sum f n) :=
begin
  induction n with n hi,
  { simp },
  { simp [partial_sum_next, hi, add_comm] }
end

lemma partial_sum_add {R : Type u} [add_comm_monoid R] (f : ℕ → R) (g : ℕ → R) (n : ℕ)
: partial_sum f n + partial_sum g n = partial_sum (λ k, f k + g k) n :=
begin
  induction n with n ih,
  { simp },
  { repeat { rw partial_sum_next },
    rw ←ih,
    abel }
end

lemma partial_sum_sub {R : Type u} [add_comm_group R] (f : ℕ → R) (g : ℕ → R) (n : ℕ)
  : partial_sum f n - partial_sum g n = partial_sum (λ k, f k - g k) n :=
begin
  induction n with n ih,
  { simp },
  { repeat { rw partial_sum_next },
    rw ←ih,
    abel }
end


lemma diff_partial_sums_of_agrees' {a b : ℕ → ℝ} {k : ℕ} (h : ∀ n : ℕ, k ≤ n → a n = b n) (n : ℕ)
  : partial_sum a (n + k) - partial_sum b (n + k) = partial_sum a k - partial_sum b k :=
begin
  induction n with n hi,
  { simp },
  have : a (n + k) + partial_sum a (n + k) - (b (n + k) + partial_sum b (n + k)) =
    (a (n + k) - b (n + k)) + (partial_sum a (n + k) - partial_sum b (n + k)) := by ring,
  simp [this, (show n + 1 + k = n + k + 1, by ring), partial_sum_next, hi, h (n + k) (le_add_self)]
end

lemma diff_partial_sums_of_agrees {a b : ℕ → ℝ} {k : ℕ} (h : ∀ n : ℕ, k ≤ n → a n = b n) {n : ℕ}
  (hn : k ≤ n) : partial_sum a n - partial_sum b n = partial_sum a k - partial_sum b k :=
begin
  have := diff_partial_sums_of_agrees' h (n - k),
  rw nat.sub_add_cancel hn at this,
  exact this,
end

lemma monotone_partial_sum_of_terms_nonneg {f : ℕ → ℝ} (h : ∀ n, 0 ≤ f n)
  : monotone (partial_sum f) :=
begin
  intros n m hnm,
  induction m with m ih,
  { rw nat.eq_zero_of_le_zero hnm },
  { by_cases hc : n = m.succ,
    { rw hc },
    { have h₁ : n ≤ m := nat.le_of_lt_succ (lt_of_le_of_ne hnm hc),
      calc partial_sum f n ≤ partial_sum f m : ih h₁
                       ... ≤ f m + partial_sum f m : by linarith [h m]
                       ... = partial_sum f (m + 1) : by rw partial_sum_next } }
end

Some of these (e.g. partial_sum_neg) could probably be generalized to functions.

[Niels Voss]

I'm just trying to formalize the most basic Riemann Series Theorem about real numbers, which is that if you have a conditionally converging series you can rearrange it to converge to an arbitrary real number, I unfortunately don't know enough to formalize the more general versions of the proof.

[Yury G. Kudryashov]

We have docs#Finset.sum_range_succ

[Yury G. Kudryashov]

docs#Finset.sum_neg_distrib

[Yury G. Kudryashov]

docs#Finset.sum_add_distrib docs#Finset.sum_sub_distrib

[Yury G. Kudryashov]

docs#Finset.sum_le_sum_of_subset_of_nonneg with docs#Finset.range_mono

[Yury G. Kudryashov]

docs#Finset.sum_range_add

[Niels Voss]

Thank you! Since I have already started working on the proof in terms of partial_sum, for now I will just use these lemmas to simplify my proofs and if I can get the theorem to be sorry-free I will replace partial_sum with (finset.range n).sum in the final proof.