# Zulip Chat Archive

## 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):

**d**ependent **i**f **t**hen **e**lse, 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