## Stream: new members

### Topic: Inequalities with Reals

#### ROCKY KAMEN-RUBIO (Apr 25 2020 at 01:34):

I'm trying to prove ¬ real.sqrt 5 = 0. I know that for nats we would just do cc, but tactics like ring don't seem to be working for me here. I'm also having trouble finding theorems in mathlib that relate to inequalities with reals, or theorems from other typeclasses that are inherited by the reals. I'm could transform this into expressions like ¬ 5 = 0 using (0:ℝ) ≤ (5:ℝ) and real.sqrt_eq_zero, but then I run into the same issue. Could someone point me in the right direction?

#### Reid Barton (Apr 25 2020 at 01:35):

The norm_num tactic will prove ¬ 5 = 0, at least.

#### Shing Tak Lam (Apr 25 2020 at 01:38):

In fact norm_num could prove your initial goal.

import tactic data.real.basic

example : ¬ real.sqrt 5 = 0 := by norm_num


#### Mario Carneiro (Apr 25 2020 at 01:42):

this is almost certainly one of those times when it's not norm_num doing the work

#### Reid Barton (Apr 25 2020 at 01:43):

@[simp] theorem sqrt_eq_zero (h : 0 ≤ x) : sqrt x = 0 ↔ x = 0

#### Mario Carneiro (Apr 25 2020 at 01:45):

aha:

example : ¬ real.sqrt 5 = 0 := by simp [
show 0 ≤ (5:ℝ), by norm_num, show (5:ℝ) ≠ 0, by norm_num]


#### Mario Carneiro (Apr 25 2020 at 01:45):

it's because norm_num calls simp with norm_num as discharger

#### ROCKY KAMEN-RUBIO (Apr 25 2020 at 20:37):

Somewhat related inequality question: I'm trying to do this pretty simple limit proof. I get this far, and I know conceptually I need to use he and the inverse of hn to finesse my goal state into something trivial, but I can't seem to get there with the theorems I know (especially with the type casting). Could someone point me in the right direction?

import data.real.basic
import data.nat.basic
import algebra.archimedean
def lim_to_inf (x : ℕ → ℝ) (l : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, abs (x n - l) < ε

example : lim_to_inf (λ n, 1/n) 0 :=
begin
rw lim_to_inf,
intro ε,
intro hε,
have he := exists_nat_gt ε,
cases he with N he,
use N,
intro n,
intro hn,
simp,
end


#### Kevin Buzzard (Apr 25 2020 at 20:54):

What if epsilon=0.1, N=1, and n=1? Then the goal is false.

#### Chris Hughes (Apr 25 2020 at 21:01):

You want a nat greater than 1/epsilon I think.

#### Kevin Buzzard (Apr 25 2020 at 21:43):

I would write down a careful paper proof first, and then think about how to get each line into Lean.

Last updated: May 13 2021 at 21:12 UTC