Zulip Chat Archive

Stream: new members

Topic: Inequalities with Reals


view this post on Zulip 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?

view this post on Zulip Reid Barton (Apr 25 2020 at 01:35):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Apr 25 2020 at 01:43):

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

view this post on Zulip 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]

view this post on Zulip Mario Carneiro (Apr 25 2020 at 01:45):

it's because norm_num calls simp with norm_num as discharger

view this post on Zulip 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 ,
have he := exists_nat_gt ε,
cases he with N he,
use N,
intro n,
intro hn,
simp,
end

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 20:54):

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

view this post on Zulip Chris Hughes (Apr 25 2020 at 21:01):

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

view this post on Zulip 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