range N and fin N

Stream: new members

[MohanadAhmed]

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]

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]

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]

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]

Thanks! that was very informative.

[Kevin Buzzard]

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]

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]

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]

Or you can use the lemma I crossed out

[MohanadAhmed]

@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]

Precisely so, yes

[Kevin Buzzard]

dite just means "if then else"

[Kevin Buzzard]

"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]

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.