How to prove the generating function of the Fibonacci?

Stream: general

[Jasin Jiang]

this is the example.

import Mathlib

open Finset Nat Real BigOperators

example (x : ℝ) : x / (1 - x - x ^ 2) = ∑' n, Nat.fib n * x ^ n := by
  sorry

[Kevin Buzzard]

That's not true -- what if x=37?

[Jasin Jiang]

Kevin Buzzard said:

That's not true -- what if x=37?

image.png
This is a natural language representation. Did I make a mistake in my Lean 4 code?

[Jasin Jiang]

In this problem, what troubles me the most is how to handle this infinite summation. I searched for relevant theorems on mathlib but still feel puzzled, as I have no prior experience dealing with this kind of problem.

[Eric Wieser]

This is another problem from "The Art of Proving Binomial Identities", right?

[Jasin Jiang]

Eric Wieser said:

This is another problem from "The Art of Proving Binomial Identities", right?

Yes, I am trying to prove some theorems from this book to improve my Lean 4 skills.

[Eric Wieser]

Are you collaborating with @Yiran Wang on this, or is it coincidence that you are both using the same resource?

[Etienne Marion]

Jasin Jiang said:

Did I make a mistake in my Lean 4 code?

The issue is that the equality only holds for x such that the series is convergent.

[Michael Stoll]

... or for formal power series.

[Julian Berman]

docs#PowerSeries.mk

[Yakov Pechersky]

We don't have evaluation of power series yet, but we have docs#FormalMultilinearSeries

[Yakov Pechersky]

And then, docs#FormalMultilinearSeries.radius and docs#FormalMultilinearSeries.sum

[Julian Berman]

Maybe I'm not following well but @Jasin Jiang are you trying to evaluate at all? Doesn't the image just say to find the generating function? I don't know what the previous line problem said but I think it's just mistated in Lean? And perhaps the intention was:

import MAthlib.Data.Nat.Fib.Basic
import Mathlib.RingTheory.PowerSeries.Inverse
import Mathlib.RingTheory.PowerSeries.WellKnown

open PowerSeries

example : mk (fun x ↦ (Nat.fib x : ℚ)) = (X : ℚ⟦X⟧) * (1 - X - X ^ 2 : ℚ⟦X⟧)⁻¹ := by
  sorry

[Jasin Jiang]

Julian Berman said:

Maybe I'm not following well but Jasin Jiang are you trying to evaluate at all? Doesn't the image just say to find the generating function? I don't know what the previous line problem said but I think it's just mistated in Lean? And perhaps the intention was:

import MAthlib.Data.Nat.Fib.Basic
import Mathlib.RingTheory.PowerSeries.Inverse
import Mathlib.RingTheory.PowerSeries.WellKnown

open PowerSeries

example : mk (fun x ↦ (Nat.fib x : ℚ)) = (X : ℚ⟦X⟧) * (1 - X - X ^ 2 : ℚ⟦X⟧)⁻¹ := by
  sorry

Hello, please wait a moment, I might need to interpret the meaning of this code. I'm just starting with Lean. :(

[Julian Berman]

You can also wait a moment for any of the many people above who know more than I do to tell us I sent you down the wrong path. But I don't think so? At least that's my reading of your image -- though I'll say that it's slightly frustrating filling in that sorry in Mathlib in my limited experience. I forget whether we got to this generating function at the NYC meetup or if we gave up by then... But it will likely depend on how your book is telling you to solve this.

[Patrick Massot]

I think they may have to wait for a very long moment if they refuse to answer Eric’s question.

[Jasin Jiang]

Eric Wieser said:

Are you collaborating with Yiran Wang on this, or is it coincidence that you are both using the same resource?

I just saw this message. This is not a coincidence; we are classmates from the same university. Our research requires the use of the Lean language, but I am not familiar with it, so I came to this forum to ask questions. Orz.

[Julian Berman]

Is this your homework then? If so you should say so when asking your question, as many of us aren't interested in doing your homework (but may be happy to give you hints).

[Jasin Jiang]

Julian Berman said:

Is this your homework then? If so you should say so when asking your question, as many of us aren't interested in doing your homework (but may be happy to give you hints).

For Lean 4 proofs, I can handle some simple problems on my own, but when I encounter new concepts, I often feel at a loss. If possible, I would appreciate some hints from everyone.

[Patrick Massot]

The hint is to work on some learning material before tackling more advanced problems. You can find a list at https://leanprover-community.github.io/learn.html

[Jz Pan]

Do you have an informal proof written down on paper?

[Jz Pan]

And try your best to explain your proof to a 7th grade middle school student.