Need some help to convert an induction blueprint to LEAN

Stream: new members

[RedPig]

I am practicing LEAN writing on the following trivial problem

Given an integer $n >1$, we define the sequence $\{a_k\}$ as $a_0 = \frac{1}{2}$ and $a_{k+1} = a_k + a_k^2/n$. Prove that $a_n > 0$.

Following the recommendation on Terrence Tao' blog, I start writing a blueprint

We prove by induction that $\forall k, a_k > 0$

• When $k= 0$ , $a_0 = 1/2 >0$.
• Assume $k$ holds, at $k+1$, we have

$$\begin{align*} a_{k+1} & = a_k + a_k^2/n \\ & > 0+ a_k^2/n \\ & \ge 0 \end{align*}$$

I am able to translate the problem into LEAN but somehow get stuck in the proof, especially related to the syntax on the induction part. What shall I do inside the second part of the induction, shall I start with another show? How can I use the induction at k? Really appreciate some help, thank you!

theorem (a: ℕ → ℝ) (n : ℕ) (h1: n>1) (h0: a 0 = 1/2) (ha : ∀ k: ℕ, a (k+1) = a k + (a k)^2/n ) : a n >0  := by
  have ha_pos : ∀ k: ℕ, a k > 0 := by
    intro k
    induction' k with k ih
    . show a 0 > 0 ; linarith
    ...

[Ilmārs Cīrulis]

(As another beginner) this is how far I got. :sweat_smile:

import Mathlib

theorem Unnamed (a: ℕ → ℝ) (n : ℕ) (h0: a 0 = 1/2) (ha : ∀ k: ℕ, a (k+1) = a k + (a k) ^ 2 / n): a n > 0  := by
  induction n with
  | zero => linarith
  | succ m iH => rw [ha]
                 sorry

[Ilmārs Cīrulis]

Ok, it seems I got it. Will post in five minutes the correct version.

[Yury G. Kudryashov]

positivity should close this goal.

[Ilmārs Cīrulis]

Thank you!

import Mathlib

theorem Unnamed (a: ℕ → ℝ) (h0: a 0 = 1/2) (ha : ∀ k: ℕ, a (k+1) = a k + (a k) ^ 2 / k): ∀ n, a n > 0  := by
  intro n
  induction n with
  | zero => linarith
  | succ m iH => rw [ha]
                 positivity

[Yury G. Kudryashov]

BTW, @RedPig please don't post the same question in two threads.

[Ilmārs Cīrulis]

Ah, my bad, I thought that n inside ha is a mistake and changed it to k. :sweat_smile:

[Ilmārs Cīrulis]

import Mathlib

theorem Unnamed (a: ℕ → ℝ) (h0: a 0 = 1/2) (n: ℕ) (Hn: n > 1) (ha : ∀ k: ℕ, a (k+1) = a k + (a k) ^ 2 / n): ∀ m, a m > 0 := by
  intro m
  induction m with
  | zero => linarith
  | succ m' iH => rw [ha]
                  positivity

theorem Goal (a: ℕ → ℝ) (h0: a 0 = 1/2) (n: ℕ) (Hn: n > 1) (ha : ∀ k: ℕ, a (k+1) = a k + (a k) ^ 2 / n): a n > 0 :=
  Unnamed a h0 n Hn ha n

I proved a bit more general theorem first (as a m > 0 for all m, because we are lucky) and then applied it to this specific case.

Is this what you want?

[RedPig]

It will be similar if the recursion is using $k$, I am using the weird structure for my own understanding on how to add dependency. A minimum change of your proof works, thank you!

theorem Unnamed (a: ℕ → ℝ) (n: ℕ) (h0: a 0 = 1/2) (ha : ∀ k: ℕ, a (k+1) = a k + (a k) ^ 2 / n): a n > 0  := by
  have ha_pos : ∀ k: ℕ, a k > 0 := by
    intro k
    induction k with
    | zero => linarith
    | succ k ih => rw [ha]
                   positivity
  use ha_pos n

[RedPig]

Yury G. Kudryashov said:

BTW, RedPig please don't post the same question in two threads.

I did not do it in purpose, I tried to ask minimum hint and complete the task by myself but I still get stuck hence asking for the entire one again. Will try to minimize that in the future.