Squaring an inequality?

Stream: new members

[James Arthur]

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

[Reid Barton]

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

[James Arthur]

I've just found apply mul_self_lt_mul_self_iff

[James Arthur]

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.

[Kevin Buzzard]

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

[James Arthur]

Thankyou, splitting seemed to be the answer

[Kenny Lau]

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

[James Arthur]

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

[James Arthur]

with help from @Shing Tak Lam