coercion in inequalities

Stream: new members

[Guy]

[reposting from Lean for teaching]

hi i'm trying to prove Bernoulli's inequality in lean.

this is what I got so far, getting into trouble handling the nat->real coercion

import tactic

import data.real.basic
import data.rat.basic
import data.nat.basic

/-
-/
open_locale classical -- allow proofs by contradiction
/-
-/
noncomputable theory -- don't fuss about the reals being noncomputable

namespace infi1

theorem bernoulli_ineq {x : ℝ} {n : ℕ} [h : x ≥ -1] : (1+x) ^ n ≥ 1 + (n * x) :=
begin
  induction n with d hd,
  rw pow_zero,
  norm_cast,
  linarith,

  have h3 : ((1 + x) ^ d) * (1+x) ≥ (1 + ↑d * x) * (1+x),
    nlinarith,

  rw nat.succ_eq_add_one,
  rw pow_add,
  rw pow_one,

  have h4 : (1 + ↑d * x) * (1 + x) ≥ 1 + ↑(d + 1) * x,
    -- what now
end

end infi1

by the end of the proof, h3 looks alot like the goal, just need to prove h4. I failed to find the right coercion dance to solve h4, would appreciate some help :^)

For example, I couldn't figure out how to prove some key points:

• ↑(d+1) = ↑d+1
• ↑d ≥ 0

[Kevin Buzzard]

Here's your proof so far, following the recommended style guide:

theorem bernoulli_ineq {x : ℝ} {n : ℕ} [h : x ≥ -1] : (1+x) ^ n ≥ 1 + (n * x) :=
begin
  induction n with d hd,
  -- you shouldn't be writing tactics when you have two open goals;
  -- use brackets to focus on an individual goal.
  { rw pow_zero,
    norm_cast,
    linarith, },
  { have h3 : ((1 + x) ^ d) * (1+x) ≥ (1 + ↑d * x) * (1+x),
    -- two goals again
    { nlinarith, },
    rw nat.succ_eq_add_one,
    rw pow_add,
    rw pow_one,
    have h4 : (1 + ↑d * x) * (1 + x) ≥ 1 + ↑(d + 1) * x,
    { sorry },
    sorry }
end

As for your questions, I'm not really sure what you're asking. "h3 looks a lot like the goal" -- yeah but h3 isn't the goal. "just need to prove h4" -- no -- you also need to prove that h3 and h4 are enough. Lean wants to see all the details, or at least be pushed in the right direction. Which step are you planning on working on next?

[Kevin Buzzard]

Oh and you shouldn't really be using ≥ -- tactics and lemmas are expecting to see ≤. Here's another rewrite (also fixing the issue Johan mentioned in the other thread):

theorem bernoulli_ineq {x : ℝ} {n : ℕ} (h : -1 ≤ x) : 1 + ((n : ℝ) * x) ≤ (1 + x) ^ n :=
begin
  induction n with d hd,
  { -- base case
    rw pow_zero,
    norm_cast,
    linarith, },
  { -- inductive step
    have h3 : (1 + ↑d * x) * (1 + x) ≤ ((1 + x) ^ d) * (1 + x),
    -- two goals again
    { nlinarith, },
    rw nat.succ_eq_add_one,
    rw pow_add,
    rw pow_one,
    have h4 : 1 + ↑(d + 1) * x ≤ (1 + ↑d * x) * (1 + x),
    { sorry },
    sorry }
end

[Kevin Buzzard]

↑(d+1) = ↑d+1 is provable with norm_cast or push_cast; 0 ≤ ↑d is provable with library_search which finds exact nat.cast_nonneg d.

[Guy]

first of all thanks for the format crash course, will definitely follow it from now.

I didn't quite understand some of what you wrote:

-- no -- you also need to prove that h3 and h4 are enough

but why?
h3 says a ≤ b
h4 says b ≤ c
goal is a ≤ c
so.. that?

[Guy]

again, if I could only prove:

• ↑(d+1) = ↑d+1
• ↑d ≥ 0

I think (n)linarith should get it?

[Guy]

sorry i missed your buttom message

[Kevin Buzzard]

so.. that?

Right! That has a name, so you can either apply the term, or you can apply a tactic which knows that fact. But it's not vacuously true -- you have to make it happen.

Aah, right: so indeed linarith will do it (that's the tactic), or you could do it directly (and much more quickly, although we're only talking milliseconds probably) using le_trans (that's the term).

[Eric Wieser]

Guy said:

again, if I could only prove ...

then add a have statement that says those things, prove them with sorry, and come back to them when you've proved the rest