sum of n and n^2 in Icc

Stream: new members

[Sabbir Rahman]

how to prove icc sum formulas like below

import Mathlib

example : (∑ i ∈ Finset.Icc 1 1000, i) = 1000 * 1001 / 2 := by sorry
example : (∑ i ∈ Finset.Icc 1 1000, i^2) = 1000 * 1001 * 2001 / 6 := by sorry

I know there is a version for Finset.range for first one, but I haven't worked with big operators or finset much so not sure how to proceed

[Kevin Buzzard]

The natural division makes things a little harder -- would you be happy with (i^2 : \Q) etc as your summands? Such a formalization would be closer to the traditional mathematical meaning; for example 1^2+2^2=31/6 in naturals, so this would be provable in Lean, but it wouldn't be true if you coerced to rationals. In particular, proving the things you suggest above doesn't immediately imply them for ratioals.

[Aaron Liu]

This is probably not what you meant, but these are also just rfl, since there are no free variables.

import Mathlib

set_option maxRecDepth 5000
example : (∑ i ∈ Finset.Icc 1 1000, i) = 1000 * 1001 / 2 := rfl
example : (∑ i ∈ Finset.Icc 1 1000, i^2) = 1000 * 1001 * 2001 / 6 := rfl

[Sabbir Rahman]

Kevin Buzzard said:

The natural division makes things a little harder -- would you be happy with (i^2 : \Q) etc as your summands? Such a formalization would be closer to the traditional mathematical meaning; for example 1^2+2^2=31/6 in naturals, so this would be provable in Lean, but it wouldn't be true if you coerced to rationals. In particular, proving the things you suggest above doesn't immediately imply them for ratioals.

Yes sure. best case scenario would be I somehow get existing mathlib theorems to do the work for me

[Sabbir Rahman]

Aaron Liu said:

This is probably not what you meant, but these are also just rfl, since there are no free variables.

ah that does solve it :D, but you're right the 1000 is not really my goal, rather it's how to transform those to known theorems

[Zhang Qinchuan]

Notice that Finset.Icc a b equals to Finset.Ico a (b+1).

variable (a b : ℕ)

#check (Nat.Ico_succ_right : ∀ a b : ℕ, Finset.Ico a (b + 1) = Finset.Icc a b)

You can use Finset.sum_Ico_eq_sum_range to transform these Finset.sum.

import Mathlib

example : ∑ i ∈ Finset.Icc 1 1000, i = ∑ i ∈ Finset.range 1001, i := by
  rw [Finset.sum_range_succ', add_zero, ← Nat.Ico_succ_right, Finset.sum_Ico_eq_sum_range]
  apply Finset.sum_congr rfl
  intros; rw [add_comm]