two_le_add_inv

Stream: Is there code for X?

[Rémy Degenne]

Do we have this?

lemma two_le_add_inv {x : ℝ} (hx : 0 < x) : 2 ≤ x + x⁻¹ := sorry

[Chris Hughes]

lemma two_le_add_inv {x : ℝ} (hx : 0 < x) : 2 ≤ x + x⁻¹ :=
le_of_mul_le_mul_left
  (sub_nonneg.1 $
    calc 0 ≤ (x - 1) ^ 2 : pow_two_nonneg _
       ... = _ : by field_simp [ne_of_gt hx]; ring)
  hx

[Rémy Degenne]

That's three lines shorter than mine :) Thanks.
Should I add it, if that exact statement is not already somewhere under another name?

[Rémy Degenne]

I guess that yes, I want to add it if it does not already exist. My original question was more "does it exist already in a place I did not find?", and not really "how do I prove this?".

[Alex J. Best]

Maybe it should go in analysis.mean_inequalities? its sortof a special case of AM-GM?

[Patrick Massot]

This has nothing to do with real or complex numbers so it should probably not go in analysis

[Patrick Massot]

It should assume a linear order field or something like this

[Yury G. Kudryashov]

Should we have AM-GM for linear ordered fields (with pow instead of root)?