Proof of simple inequality

Stream: new members

[Alex Gu]

I was trying to prove the following inequality
image.png

I came up with the following proof, but it seems overly verbose, and I suspect things could be made much simpler. Could somebody suggest places I could have simplified things? Thanks a lot!

theorem inequality (x y z : ℝ)
    (hx : x > 1) (hy : y > 1) (hz : z > 1)
    (h : 1/x + 1/y + 1/z = 2) :
    √(x + y + z) ≥ √(x - 1) + √(y - 1) + √(z - 1) := by

  suffices x + y + z ≥ (√(x - 1) + √(y - 1) + √(z - 1))^2 by
    have h : Real.sqrt (x + y + z) ≥ Real.sqrt ((√(x - 1) + √(y - 1) + √(z - 1))^2) := Real.sqrt_le_sqrt this
    rw [Real.sqrt_sq] at h
    exact h
    apply add_nonneg
    apply add_nonneg
    all_goals apply Real.sqrt_nonneg

  have h : (x-1)/x+(y-1)/y+(z-1)/z = 1 := by
    rw [sub_div, sub_div, sub_div]
    rw [div_self, div_self, div_self]
    linarith
    all_goals linarith

  suffices (x + y + z) * ((x-1)/x+(y-1)/y+(z-1)/z) ≥ (√(x-1)+√(y-1)+√(z-1))^2 by
    rw [h] at this
    linarith

  convert_to (∑ i : Fin 3, (![√x, √y, √z] i)^2) * (∑ i : Fin 3, (![√((x-1)/x), √((y-1)/y), √((z-1)/z)] i)^2) ≥ (∑ i : Fin 3, ![√x, √y, √z] i * (![√((x-1)/x), √((y-1)/y), √((z-1)/z)] i))^2
  · simp [Fin.sum_univ_three]
    rw [Real.sq_sqrt, Real.sq_sqrt, Real.sq_sqrt, Real.sq_sqrt, Real.sq_sqrt, Real.sq_sqrt]
    rw [sub_div, div_self]
    rw [sub_nonneg]
    rw [one_div_le]
    linarith; linarith; linarith; linarith
    rw [sub_div, div_self]
    rw [sub_nonneg]
    rw [one_div_le]
    linarith; linarith; linarith; linarith
    rw [sub_div, div_self]
    rw [sub_nonneg]
    rw [one_div_le]
    linarith; linarith; linarith; linarith
    linarith; linarith; linarith
  . simp [Fin.sum_univ_three]
    congr
    rw [<- Real.sqrt_mul']
    congr
    field_simp
    rw [sub_div, div_self, sub_nonneg, one_div_le, one_div_one]
    linarith; linarith; linarith; linarith
    field_simp
    field_simp

  apply Finset.sum_mul_sq_le_sq_mul_sq

[Yuyuan (Lance) Ouyang]

Other experts should simplify much better, but below is just my attempts based on my limited understanding.

import Mathlib

theorem inequality (x y z : ℝ)
    (hx : x > 1) (hy : y > 1) (hz : z > 1)
    (h : 1/x + 1/y + 1/z = 2) :
    √(x + y + z) ≥ √(x - 1) + √(y - 1) + √(z - 1) := by

  suffices x + y + z ≥ (√(x - 1) + √(y - 1) + √(z - 1))^2 by
    exact Real.le_sqrt_of_sq_le this

  have h : (x-1)/x+(y-1)/y+(z-1)/z = 1 := by
    field_simp
    field_simp at h
    linarith

  suffices (x + y + z) * ((x-1)/x+(y-1)/y+(z-1)/z) ≥ (√(x-1)+√(y-1)+√(z-1))^2 by
    rw [h] at this
    linarith

  convert_to (∑ i : Fin 3, (![√x, √y, √z] i)^2) * (∑ i : Fin 3, (![√((x-1)/x), √((y-1)/y), √((z-1)/z)] i)^2) ≥ (∑ i : Fin 3, ![√x, √y, √z] i * (![√((x-1)/x), √((y-1)/y), √((z-1)/z)] i))^2
  · simp [Fin.sum_univ_three]
    field_simp
    rw [Real.sq_sqrt, Real.sq_sqrt, Real.sq_sqrt]
    all_goals simp
    all_goals linarith
  . simp [Fin.sum_univ_three]
    field_simp

  apply Finset.sum_mul_sq_le_sq_mul_sq