mixing real and natural numbers

Stream: new members

[Jayden Vap]

Hello, I am new to Lean, and I am attempting to do an inductive proof. The variable that I am doing induction on is a natural number, but in one part of the equation, the variable is seen as a real number because it is being multiplied to a real number. For the base case, is there a way to have lean read that variable as a natual number so it can be reduced? I hope this makes sense, thank you

[Ruben Van de Velde]

I don't follow - can you paste a #mwe?

[Jayden Vap]

theorem inductionProblemV1
(m: ℕ) (x: ℝ) (hn: m >=2) (h1x: x >-1)(h2x: x ≠ 0): (1+x)^(m+2)> 1 + (m+2)*x :=

[Mario Carneiro]

See the #mwe page, and #backticks

[David Renshaw]

If you want spoilers on how mathlib proves a similar inequality: https://leanprover-community.github.io/mathlib_docs/algebra/group_power/lemmas.html#one_add_mul_le_pow

[Jayden Vap]

theorem  inductionProblemV1
 (m: ℕ) (x: ℝ) (hn: m >=2) (h1x: x >-1)(h2x: x ≠ 0): (1+x)^(m+2)> 1 + (m+2)*x :=

[Eric Wieser]

Does induction m not work as a first step?

[Jayden Vap]

It does, but I am having difficulty reducing m on the righr side of the inequality for the base case because 0 is a real number in this case... maybe theres a simple solution but zero_add does not work when 0 is a real

[Gihan Marasingha]

For the base case, I'd just use the linarith tactic (unless you think that's cheating).

[Mario Carneiro]

Here's an #mwe with a bit more progress:

import data.real.basic

theorem inductionProblemV1
  (m: ℕ) (x: ℝ) (hn: m ≥ 2) (h1x: x > -1) (h2x: x ≠ 0) : (1+x)^(m+2)> 1 + (m+2)*x :=
begin
  induction m,
  { simp,
    -- ⊢ 1 + 2 * x < (1 + x) ^ 2
    sorry },
  { sorry }
end

[Mario Carneiro]

simp cleans up the coercion in the zero case

[Huỳnh Trần Khanh]

norm_num should work right? like norm_num should clean up the coercions right

[Huỳnh Trần Khanh]

but yeah I'd just use a sledgehammer (ring, linarith, simp) to demolish the base case

[Kevin Buzzard]

I am suspicious about the hypothesis m>=2 and the occurrences of m+2 in the goal. Are we sure we're proving the correct statement here?

[Kevin Buzzard]

For example the statement seems to be true for m=0

[Gihan Marasingha]

@Kevin Buzzard I proved the result and my first step was clear hn. Otherwise this messes up the induction!

[Jayden Vap]

It should be m=0, my mistake

[Kevin Buzzard]

Please post an #mwe to explain precisely what you mean.

[Gihan Marasingha]

This can be filled in, but linarith no longer solves the base case:

 theorem  inductionProblemV1 (m : ℕ) (x : ℝ) (hn : 2 ≤ m)
  (h1x : -1 < x) (h2x : x ≠ 0) : (1 + x)^(m + 2) > 1 + (m + 2) * x :=
 begin
    clear hn,
    induction m with k ih,
    { sorry },
    { sorry },
 end

[Shadman Sakib]

what is the distribution command on lean vs?
for something like (a+b) *(a-b)

[Adam Topaz]

@Shadman Sakib toward the bottom of the zulip window, you will see a "new topic" button. Please use that to create a new topic for this question (in the new members stream)

[Eric Wieser]

Or better yet, click the edit (pencil?) icon and edit your message title to something new

[Eric Wieser]

@Bryan Gin-ge Chen mind moving these messages too?