Induction on sum of geometric series

Stream: maths

[Divya Ranjan]

I've been trying to write proof of this theorem in Lean4, and for some reason the base case seems to be behaving weirdly. I've reduced the required expression to be $a=a$ but doing rfl brings up another goal $r - 1 \neq 0$.

[Divya Ranjan]

https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQEwCmAdnAGLBEDOB8AQsAOYDyhUK0lehJAShQzhwEAHknDoCcAN5I4UOAC44gXEIAvnAAUJJYFRCAJSbUiuXEAGRHACMBpYEQiOMDiAIIjlIiDSVoDUVgDRxZAFRyAHoOALyagSFeVnAAtP4GAPSaUHGxChFYAJ44cPZEACYArgDGMMAQJCQA7sBo9qh5cAA+cABeBFAQcGEAfHBEaAD6UDWWcADalMUgo67uw1UEfpA1w53dfiDF6EtEBAC6ANzN+ecXcuOTmxDDSIWFqxDryydwZ5cXQ6ij4wDMU0ACYRwHZ7Zb+E6fL75MbA0G7YYzLB+EFg4aFYAANz8mKxSII6AAZu9oTCyV9mm0ZqVSoM4MNegM4JRoFBsj5BM0gA

[David Loeffler]

Please post the actual code rather than a link.

[Divya Ranjan]

David Loeffler, apologies. My first post here, wasn't aware of the convention.

[Divya Ranjan]

import Mathlib

open Finset BigOperators

example {a r : ℝ} (n : ℕ) (h : r ≠ 1) : ∑ i ∈ range (n+1), a * r^i = (a * r^(n+1) - a) / (r-1) := by

induction n with ih

| zero => nth_rw 1 [sum_range_one, pow_zero, mul_one];

rw [zero_add, pow_one];

nth_rw 3 [← mul_one a];

rw [← mul_sub, ← mul_div, div_self];

| succ n _ => sorry,

[Kevin Buzzard]

import Mathlib
open Finset BigOperators
open Ring

example {a r : ℝ} (n : ℕ) (h : r ≠ 1) : ∑ i ∈ range (n+1), a * r^i = (a * r^(n+1) - a) / (r-1) := by
  induction n with -- (minor edit here)
  | zero => nth_rw 1 [sum_range_one, pow_zero, mul_one]
            rw [zero_add, pow_one]
            nth_rw 3 [← mul_one a]
            rw [← mul_sub, ← mul_div, div_self]
            sorry
            sorry -- second `sorry` needed to get the code error-free

  | succ n _ =>  sorry -- (minor edit here)

After rw [div_self] you have two goals not one, because div_self needs the hypothesis $r-1\not=0$ to apply. So things are working as expected. Note also I removed the spurious ih after with on the induction line, and the comma at the end (those are lean 3-isms)

[Kevin Buzzard]

Kevin Buzzard said:

import Mathlib
open Finset BigOperators
open Ring

example {a r : ℝ} (n : ℕ) (h : r ≠ 1) : ∑ i ∈ range (n+1), a * r^i = (a * r^(n+1) - a) / (r-1) := by
  induction n with -- (minor edit here)
  | zero => nth_rw 1 [sum_range_one, pow_zero, mul_one]
            rw [zero_add, pow_one]
            nth_rw 3 [← mul_one a]
            rw [← mul_sub, ← mul_div, div_self]
            sorry
            sorry -- second `sorry` needed to get the code error-free

  | succ n _ =>  sorry -- (minor edit here)

After rw [div_self] you have two goals not one, because div_self needs the hypothesis $r-1\not=0$ to apply (in Lean 0/0=0). So things are working as expected. Note also I removed the spurious ih after with on the induction line, and the comma at the end (those are lean 3-isms)

[Divya Ranjan]

@Kevin Buzzard Okay, so adding an apply h after the rw should resolve it?

[Kevin Buzzard]

Well no, because r ≠ 1 isn't exactly identical to r - 1 ≠ 0 to Lean, even though as a mathematician you might say these were "basically obviously the same thing".

[Kevin Buzzard]

I'm far too busy a person to be doing all this rw [mul_one] stuff, here's how I'd do the base case:

import Mathlib
open Finset BigOperators
open Ring

example {a r : ℝ} (n : ℕ) (h : r ≠ 1) : ∑ i ∈ range (n+1), a * r^i = (a * r^(n+1) - a) / (r-1) := by
  induction n with
  | zero =>
    -- make explicit the fact that we're not dividing by 0
    have h2 : r - 1 ≠ 0 := by exact? -- find the theorem in the library saying that `r ≠ 1 → r - 1 ≠ 0`
    field_simp -- now clear denominators (this tactic looks at the local context so sees `h2`)
    ring -- solve the problem with an appropriate high-powered tactic now there's no divisions so it's a question in the language of rings
  | succ n _ =>  sorry

But if you like doing it the hands-on way then you can do it the way you did it. Different people have different motivations for why they want to prove results like this.

[Kevin Buzzard]

Note that exact? returns Try this: exact sub_ne_zero_of_ne h which is the theorem that you need to apply in your approach (and looking at the name, you can try to guess what this theorem says).

[Divya Ranjan]

Kevin Buzzard said:

Well no, because r ≠ 1 isn't exactly identical to r - 1 ≠ 0 to Lean, even though as a mathematician you might say these were "basically obviously the same thing".

Interesting, is this because from a constructive/intuitionist perspective you can't claim directly that if $r \neq 1$ it doesn't necessarily have to satisfy the $r - 1 \neq 0$ condition. But yeah from an "usual" way of doing math proofs, it makes sense since for any r other than 1, that's trivially true.

[Kevin Buzzard]

No it's nothing to do with constructivism. It's just that $r\not=1$ and $r-1\not=0$ are not literally the same thing, you have to do one line of mathematics to get from one to the other, as opposed to 0 lines of mathematics.

[Kevin Buzzard]

And that line of mathematics is called docs#sub_ne_zero_of_ne , and if you look in the source code you will see it has a one line proof.

[Divya Ranjan]

Kevin Buzzard said:

Note that exact? returns Try this: exact sub_ne_zero_of_ne h which is the theorem that you need to apply in your approach (and looking at the name, you can try to guess what this theorem says).

Interesting, thank you for the simplification. I come from doing years of hand-written proofs, so I'm trying to do it in Lean4 according to what my thinking process is. I'm yet to get used to the Lean4-fu, but any suggestions you might give on how to know if a particular hypothesis can't be trivially accepted or how to specifically get a theorem relevant to the goal. I've tried exact? and apply? but it sometimes gives irrelevant theorems/tactics.

[Divya Ranjan]

Kevin Buzzard said:

Kevin Buzzard said:

import Mathlib
open Finset BigOperators
open Ring

example {a r : ℝ} (n : ℕ) (h : r ≠ 1) : ∑ i ∈ range (n+1), a * r^i = (a * r^(n+1) - a) / (r-1) := by
  induction n with -- (minor edit here)
  | zero => nth_rw 1 [sum_range_one, pow_zero, mul_one]
            rw [zero_add, pow_one]
            nth_rw 3 [← mul_one a]
            rw [← mul_sub, ← mul_div, div_self]
            sorry
            sorry -- second `sorry` needed to get the code error-free

  | succ n _ =>  sorry -- (minor edit here)

After rw [div_self] you have two goals not one, because div_self needs the hypothesis $r-1\not=0$ to apply (in Lean 0/0=0). So things are working as expected. Note also I removed the spurious ih after with on the induction line, and the comma at the end (those are lean 3-isms)

Also with regards to the Lean3-ism, I was confused with that because of the certain proofs are mentioned in Mathematics in Lean text, it provides several proofs using this methodology, which I was unable to find in Theorem Proving in Lean and thus a bit confusing. Can/should this be changed? Is this something for which an issue might be reported in the book's Github repository?

[Kevin Buzzard]

I'm a bit confused about what we're talking about. I demonstrated how to use exact? above. As for books, which of the two books are you talking about and what exactly are you confused about?

[Divya Ranjan]

Kevin Buzzard said:

I'm a bit confused about what we're talking about. I demonstrated how to use exact? above. As for books, which of the two books are you talking about and what exactly are you confused about?

Apologies, I am not confused from your responses, I'm describing why I was confused and used induction n with ih because the Mathematics in Lean book uses proofs in this manner.

[Kevin Buzzard]

By "lean 3-ism" I meant "induction n with ih" and ",", and I would be surprised if either of these phrases occurred in either of the books

[Kevin Buzzard]

Can you show me specifically where you're seeing induction n with ih in #mil ?

[Divya Ranjan]

Kevin Buzzard said:

By "lean 3-ism" I meant "induction n with ih" and ",", and I would be surprised if either of these phrases occurred in either of the books

Check theorems fac_pos and dvd_fac here:
https://leanprover-community.github.io/mathematics_in_lean/C05_Elementary_Number_Theory.html#induction-and-recursion

[Kevin Buzzard]

That says induction' not induction. induction' is a different tactic with a different syntax.

[Kevin Buzzard]

Computers are fussy. The syntax for those tactics is completely different, just like lean thinks $r-1\ne0$ and $r\ne1$ are completely different.

[Divya Ranjan]

Ah! Okay, my bad then. I thought they are similar like others with a quote are similar. Thank you for clearing this misconception.

[Kevin Buzzard]

In fact the motivation for induction' was during the port from Lean 3 to Lean 4, because the Lean 3 syntax for induction is the same as the Lean 4 syntax for induction' whereas Lean 4 induction is very different with these |s etc.

[Divya Ranjan]

Sorry to bother you again @Kevin Buzzard , but I'm trying to find a theorem that shows:
$\sum^{n+1}_{i=1} f(n) = \sum^{n}_{i=i} f (n) + f(n+1)$. I found sum_range, sum_range_succ and sum_range_induction but I don't think they're exactly proving the aforementioned statement. Any hint/idea?

[Kevin Buzzard]

I would recommend starting at 0, not 1 :-) Then docs#Finset.sum_range_succ is (probably) exactly what you want (there seem to be several typos in your informal statement). If you really do want to start at 1, then I recommend that you ask your question again, not "informally" as above, but formally as a #mwe with a sorry, and ask the community how to fill in the sorry. Another subtlety with formalization is that for every way of asking a question informally there can be two or even more ways of asking the same question formally, so details really do matter. With a #mwe all ambiguity is gone.

[Divya Ranjan]

Kevin Buzzard said:

I would recommend starting at 0, not 1 :-) Then docs#Finset.sum_range_succ is (probably) exactly what you want (there seem to be several typos in your informal statement). If you really do want to start at 1, then I recommend that you ask your question again, not "informally" as above, but formally as a #mwe with a sorry, and ask the community how to fill in the sorry. Another subtlety with formalization is that for every way of asking a question informally there can be two or even more ways of asking the same question formally, so details really do matter. With a #mwe all ambiguity is gone.

Apologies, the habit of starting from 1 is pretty persistent. I did intend to start with 0. And yes, sum_range_succ works, I forgot that I needed $r^0$. Thank you for the tip on #mwe, I shall keep that in mind wen making further inquiries.