## Stream: new members

### Topic: coercion in inequalities

#### Guy (Dec 10 2022 at 17:41):

[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 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 (Dec 10 2022 at 17:43):

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 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 (Dec 10 2022 at 17:45):

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 pow_one,
have h4 : 1 + ↑(d + 1) * x ≤ (1 + ↑d * x) * (1 + x),
{ sorry },
sorry }
end


#### Kevin Buzzard (Dec 10 2022 at 17:49):

↑(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 (Dec 10 2022 at 17:53):

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 (Dec 10 2022 at 17:54):

again, if I could only prove:

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

I think (n)linarith should get it?

#### Guy (Dec 10 2022 at 17:56):

sorry i missed your buttom message

#### Kevin Buzzard (Dec 10 2022 at 17:56):

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 (Dec 10 2022 at 18:00):

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

Last updated: Dec 20 2023 at 11:08 UTC