Proving inequalities

Stream: new members

[Moti Ben-Ari]

In this program mul_lt_mul_left seems to be the theorem I want to use but I can't get it to work with the hypotheses that I previously proved.

import Mathlib.Tactic
def fib : ℕ → ℚ
  | 0 => 0
  | 1 => 1
  | n + 2 => fib (n + 1) + fib n
theorem seven_fourths (n : ℕ) : fib n < (7 / 4 : ℚ) ^ n := by
  induction' n using Nat.twoStepInduction with k ih1 ih2
  ·  rw [fib]
     norm_num
  ·  rw [fib]
     norm_num
  · have h1 : 0 < (7/4)^k := by norm_num
    have h2 : 1+(7/4:ℚ) < (7/4)^2 := by norm_num
    calc fib (k + 2) = fib (k + 1) + fib k := by rw [fib]
       _ < (7/4)^(k+1) + (7/4)^k := by rel [ih1, ih2]
       _ = (7/4)^k + (7/4)^k * (7/4:ℚ) := by rw [pow_add,pow_one,add_comm]
       _ = (7/4)^k * (1+(7/4)) := by rw [← mul_one_add]
       _ < (7/4)^k * (7/4)^2 := by apply mul_lt_mul_left.mpr h1 h2
       _ = (7/4)^(k+2) := by rw [← pow_add]
  done

[Yakov Pechersky]

I think you need (mul_lt_mul_left h1).mpr h2

[Yakov Pechersky]

The 0 < a hypothesis is an argument to the mul_lt_mul_left lemma.

[Patrick Massot]

You didn't give any context so maybe you have pedagogical constraints and my comment will be useless, but let me try anyway: the idiomatic way of writing this proof is:

import Mathlib.Tactic
def fib : ℕ → ℚ
  | 0 => 0
  | 1 => 1
  | n + 2 => fib (n + 1) + fib n

theorem seven_fourths (n : ℕ) : fib n < (7 / 4 : ℚ) ^ n := by
  induction' n using Nat.twoStepInduction with k ih1 ih2
  ·  rw [fib]
     norm_num
  ·  rw [fib]
     norm_num
  · calc fib (k + 2) = fib (k + 1) + fib k := by rw [fib]
       _ < (7/4)^(k+1) + (7/4)^k := by gcongr
       _ = (7/4)^k * (1+(7/4)) := by ring
       _ < (7/4)^k * (7/4)^2 := by gcongr ; norm_num
       _ = (7/4)^(k+2) := by ring
  done

[Moti Ben-Ari]

Thanks @Yakov Pechersky , it worked after I fixed up have h1 : 0 < (7/4:ℚ)^k := by apply pow_pos ; norm_num

@Patrick Massot The context is that I didn't know about gcongr! It appears only in one program in chapter 6 of MIL and not at all in TPIN, MOP, FM, HTPIWL, so I'm not surprised that I never learned it.

[Heather Macbeth]

The teaching version of gcongr is rel and this is ubiquitous in MOP.

[Patrick Massot]

About MIL: we are aware of the issue. I've been meaning to write a proper chapter about calculations since last summer, but time is very scarce and there are lots of projects.