## Stream: new members

### Topic: range N and fin N

#### MohanadAhmed (Apr 19 2023 at 15:17):

Hello everyone,
I am trying to understand the correspondence between range N and fin N. As far as I understand these two are the same, but I can't figure out how to move one to the other.

For example in mathlib the geometirc sum is written in terms of algebra.geom_sum. If I have a sum over fin N how can I use the geometric sum formula.

The code below contains a general sum and a geometric sum but with the sum in terms of fin: N instead of range N.

lemma sum_finN_sum_rangeN {N:ℕ} (f: ℕ → ℂ):
∑ (i : fin N), f i = ∑ i in (range N), f i :=
begin
induction N with N hN,
-- The case of N = 0. Both sides are zero
simp only [fintype.univ_of_is_empty, finset.sum_empty, range_zero],

-- The case of N = succ something
sorry,
end

lemma geom_sum_finN {N:ℕ} {hN: 1 < N} (α: ℂ) (hα: α ≠ 1) :
∑ (i : fin N), α ^ (i:ℕ) = (α^N - 1) / (α - 1) :=
begin
-- rw geom_sum_eq, -- This of course does not work!
sorry,
end


Thanks!

#### Eric Rodriguez (Apr 19 2023 at 15:19):

range n is a finite subset of ℕ. It is a term of type finset ℕ. fin n is a type in and of itself.

#### Eric Rodriguez (Apr 19 2023 at 15:20):

docs#finset.sum_fin_eq_sum_range docs#fin.sum_univ_eq_sum_range { is the theorem that links both together (notice that the name is very guessable)

#### Eric Rodriguez (Apr 19 2023 at 15:21):

Also note that in your sum, the i in f i has an arrow before it (if you look at the infoview). This is because Lean is automatically converting the i from a fin n into a natural number using a system called a coercion.

#### MohanadAhmed (Apr 19 2023 at 15:37):

Thanks! that was very informative.

#### Kevin Buzzard (Apr 19 2023 at 17:56):

I guess one subtle difference in this context is that if you want to sum f over range n then f needs to be defined on all naturals, whereas if you only want to sum f over fin n then f only needs to be defined on fin n.

#### MohanadAhmed (Apr 19 2023 at 19:06):

Kevin Buzzard said:

I guess one subtle difference in this context is that if you want to sum f over range n then f needs to be defined on all naturals, whereas if you only want to sum f over fin n then f only needs to be defined on fin n.

So if I understand correctly, refuses the following lemma because the function is expected to map fin N to \C. So is there a way to go the other way round i.e. force a function that takes naturals to take fin N?

lemma sum_finN_sum_rangeN {N:ℕ} (f: (fin N) → ℂ):
∑ (i : fin N), f i = ∑ i in (range N), (f  i) :=
begin
sorry,
end


#### Yaël Dillies (Apr 19 2023 at 19:11):

You will have to define f outside of range N. It shouldn't matter what you define it to be, but you'll need something.

#### Eric Rodriguez (Apr 19 2023 at 19:14):

Or you can use the lemma I crossed out

#### MohanadAhmed (Apr 19 2023 at 19:22):

@Eric Rodriguez
In the lemma you crossed out, the following scary looking statement is the part Yael is talking about (I am guessing it defines outside fin N to be zero)?

λ (i : ℕ), dite (i < n) (λ (h : i < n), c ⟨i, h⟩) (λ (h : ¬i < n), 0)


#### Eric Rodriguez (Apr 19 2023 at 19:24):

Precisely so, yes

#### Kevin Buzzard (Apr 19 2023 at 20:08):

dite just means "if then else"

#### Kevin Buzzard (Apr 19 2023 at 20:10):

"if i < n the evaluate c on i else 0". The idea is that to make a term of type Fin N you have to give a pair of pieces of data -- first a natural number, and second a proof that it's less than N. That's what ⟨i, h⟩ is. In particular, an element of Fin N is not "a natural number" -- it is a pair.

#### Yaël Dillies (Apr 19 2023 at 20:10):

dependent if then else, to be precide. The "dependent bit refers to the fact that the branches are allowed to use the proofs of p or of ¬p.

Last updated: Dec 20 2023 at 11:08 UTC