Zulip Chat Archive

Stream: new members

Topic: Squaring an inequality?


view this post on Zulip James Arthur (Aug 15 2020 at 14:07):

As part of a larger proof, inverse hyperbolic trig, I have the following lemma. Basically I want to square both sides, but I don't think thats mathematically possible? Does lean have a little thing that makes this simpler?

lemma b_lt_sqrt_b_sq_add_one (b : ) : b < sqrt(b ^ 2 + 1) :=
begin
  -- I want to square this, but I don't think thats possible.
  -- then do linaarith
  sorry
end

view this post on Zulip Reid Barton (Aug 15 2020 at 14:08):

You want to find a lemma that says (under some side conditions) a < b <-> a^2 < b^2 (or maybe a*a < b*b)

view this post on Zulip James Arthur (Aug 15 2020 at 14:11):

I've just found apply mul_self_lt_mul_self_iff

view this post on Zulip James Arthur (Aug 15 2020 at 14:13):

However, my main lemma is sinh_surjective which just said sinh is surjective and thats not only for positives, the lemma is true for all x.

view this post on Zulip Kevin Buzzard (Aug 15 2020 at 14:31):

Then you should split into two cases b<=0 and b>0

view this post on Zulip James Arthur (Aug 15 2020 at 15:23):

Thankyou, splitting seemed to be the answer

view this post on Zulip Kenny Lau (Aug 15 2020 at 17:15):

b \le abs b = sqrt (b ^ 2) < sqrt (b ^ 2 + 1) is the answer @James Arthur

view this post on Zulip James Arthur (Aug 15 2020 at 17:32):

For reference, here is the code that I ended up using:

lemma b_lt_sqrt_b_sq_add_one ( b : ) : b < sqrt(b^2 + 1) :=
begin
  by_cases hb : 0  b,
  conv {to_lhs, rw  sqrt_sqr hb},
  rw sqrt_lt,
  linarith,
  apply pow_two_nonneg,
  have F : 0  b^2 := by {apply pow_two_nonneg},
  linarith,
  rw not_le at hb,
  apply lt_of_lt_of_le hb,
  apply sqrt_nonneg,
end

view this post on Zulip James Arthur (Aug 15 2020 at 17:32):

with help from @Shing Tak Lam


Last updated: May 13 2021 at 20:13 UTC