summation

Stream: general

[Anas Himmi]

Hi, i am trying to implement the summation.
I first did this and it worked

def sigma_sum : ℕ → ℕ → (ℕ → ℤ) → ℤ
| 0 0 f := f 0
| 0 (n+1) f := sigma_sum 0 n f + f (n+1)
| (i+1) 0 f := 0
| (i+1) (n+1) f := if (i+1)>(n+1) then 0 else sigma_sum (i+1) n f + f (n+1)

but then i found it really hard to prove simple theorems such as

theorem sigma_sum_chasles {i n s : ℕ} (f : ℕ → ℤ) (his : i ≤ s) (hsn : s ≤ n) :
  sigma_sum i n f = sigma_sum i s f + sigma_sum (s+1) n f :=sorry

or

theorem succ_sigma_sum {i n : ℕ} (f : ℕ → ℤ) (h : n ≥ i) : sigma_sum (i+1) n f + f i = sigma_sum i n f :=sorry

so i tried changing the definition to something simpler like this:

def sigma_sum2 (i n : ℕ) (f : ℕ → ℤ) : ℤ :=
match n-i with
  | 0 := if n=i then f n else 0
  | (k+1) := sigma_sum2 i (n-1) f + f n
end

but sadly i get an error message unknown identifier 'sigma_sum2'

do you have any idea how to fix this?

[Scott Morrison]

You need to move n "after the colon" in order to make a recursive definition.

[Anas Himmi]

like this? i get the same error

def sigma_sum2 : ℕ → ℕ → (ℕ → ℤ) → ℤ :=
λ n i f,match n-i with
  | 0 := if n=i then f n else 0
  | (k+1) := sigma_sum2 i (n-1) f + f n
end

[Yury G. Kudryashov]

Please use ```lean

[Yury G. Kudryashov]

To enable syntax highlighting

[Anas Himmi]

sorry i fixed that

[Reid Barton]

You need to use the equation compiler (like your original version), not match.

[Scott Morrison]

def sigma_sum2 (i : ℕ) (f : ℕ → ℤ) : ℕ → ℤ
| 0 := ...
| (n+1) := ...

[Yury G. Kudryashov]

Is it ok for you to use existing mathlib functions?

[Yury G. Kudryashov]

If yes, then you can use finset.Ico with finset.sum

[Anas Himmi]

i will look into that

[Anas Himmi]

i can't find finset.sum in the library

[Johan Commelin]

@anas himmi It's in algebra/big_operators.lean

[Anas Himmi]

Thanks!