Struggle in writing LEAN proof for Nesbitt's Inequality

Stream: new members

[RedPig]

I have written the following informal proof of the N and I struggle in simple transformation in LEAN4, I have decomposed the proof into step by step but not sure how to do every single step...

Problem (Nesbitt's Inequality)
For positive reals a,b,c, prove that

$$\frac{a}{b+c} + \frac{b}{c+a} + \frac{c}{a+b} \geq \frac{3}{2}.$$

theorem nesbitt_inequality
  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) :
  a / (b + c) + b / (c + a) + c / (a + b) ≥ 3 / 2 := by sorry

Solution: By adding $1$ on each term on the LHS, we the inequality is equivalent to
$(\frac{a}{b+c} + 1) + (\frac{b}{c+a}+ 1) + (\frac{c}{a+b}+ 1) \geq \frac{3}{2}+ 3$
Expanding it gives
$\frac{a+b+c}{b+c} + \frac{b+c+a}{c+a} + \frac{c+a+b}{a+b} \geq \frac{9}{2}$
Factorizing it gives
$(a+b+c) (\frac{1}{b+c} + \frac{1}{c+a} + \frac{1}{a+b} )\geq \frac{9}{2}$
Multiply both sides by $2$ yields
$2(a+b+c) (\frac{1}{b+c} + \frac{1}{c+a} + \frac{1}{a+b} )\geq 9$
It suffices to rewrite it as
$((b+c) + (c+a) + (a+b)) (\frac{1}{b+c} + \frac{1}{c+a} + \frac{1}{a+b} )\geq (1+1+1)^2$
which is exactly Cauchy Schwartz.

[Julian Berman]

Step one is to write the statement in Lean undoubtedly. Do you have that done?

[RedPig]

yes, here is the statement in LEAN4:

theorem nesbitt_inequality
  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) :
  a / (b + c) + b / (c + a) + c / (a + b) ≥ 3 / 2 := by sorry

I also have minimal knowledge on what to apply, for instance, we need to use fileds_simp to do addition with the fractions, ring to do commutative simplification on addition. What I am struggling is how to do it on both side of the inequalities

[Daniel Weber]

You can use linarith to do simple linear parts, and suffice to change the goal:
suffices (a / (b + c) + 1) + (b / (c + a) + 1) + (c / (a + b) + 1) ≥ 9 / 2 by linarith
To do the factorization you can use covert_to, to change (a / (b + c) + 1) + (b / (c + a) + 1) + (c / (a + b) + 1) to (a + b + c) * (1 / (b + c) + 1 / (c + a) + 1 / (a + b)). To prove equality you can rewrite with docs#div_add_one and then use ring to resolve the equation. Using div_add_one requires showing that the denominators are nonzero, you can use linarith for that.
Then you can do the multiplication by 2 using linarith again: suffices ((b + c) + (c + a) + (a + b)) * (1 / (b + c) + 1 / (c + a) + 1 / (a + b)) ≥ (1 + 1 + 1)^2 by linarith.
Using Cauchy-Schwartz is a bit complicated, but you can rewrite the equation as (∑ x : Fin 3, (![√(b+c), √(c+a), √(a+b)] x)^2) * (∑ x : Fin 3, (1 / ![√(b+c), √(c+a), √(a+b)] x)^2) ≥ (∑ x : Fin 3, ![√(b+c), √(c+a), √(a+b)] x * (1 / ![√(b+c), √(c+a), √(a+b)] x))^2 (again, using convert_to). To prove equality you can use docs#Real.sq_sqrt and docs#mul_inv_cancel₀.
Finally, you can apply Cauchy-Schwartz, docs#Finset.sum_mul_sq_le_sq_mul_sq.

Together you get

import Mathlib

theorem nesbitt_inequality (a b c : ℝ) (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) :
    a / (b + c) + b / (c + a) + c / (a + b) ≥ 3 / 2 := by
  suffices (a / (b + c) + 1) + (b / (c + a) + 1) + (c / (a + b) + 1) ≥ 9 / 2 by linarith
  convert_to (a + b + c) * (1 / (b + c) + 1 / (c + a) + 1 / (a + b)) ≥ 9 / 2
  · rw [div_add_one, div_add_one, div_add_one]
    ring
    all_goals linarith
  suffices ((b + c) + (c + a) + (a + b)) * (1 / (b + c) + 1 / (c + a) + 1 / (a + b)) ≥ (1 + 1 + 1)^2 by linarith
  convert_to (∑ x : Fin 3, (![√(b+c), √(c+a), √(a+b)] x)^2) * (∑ x : Fin 3, (1 / ![√(b+c), √(c+a), √(a+b)] x)^2) ≥ (∑ x : Fin 3, ![√(b+c), √(c+a), √(a+b)] x * (1 / ![√(b+c), √(c+a), √(a+b)] x))^2
  · simp only [one_div, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.sum_univ_three, Fin.isValue,
    Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons, Matrix.cons_val_two,
    Matrix.tail_cons, inv_pow]
    rw [Real.sq_sqrt, Real.sq_sqrt, Real.sq_sqrt] <;> linarith
  · simp only [Nat.succ_eq_add_one, Nat.reduceAdd, one_div, Fin.sum_univ_three, Fin.isValue,
    Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons, Matrix.cons_val_two,
    Matrix.tail_cons]
    rw [mul_inv_cancel₀, mul_inv_cancel₀, mul_inv_cancel₀] <;> (rw [Real.sqrt_ne_zero']; linarith)
  apply Finset.sum_mul_sq_le_sq_mul_sq

[Julian Berman]

I can't quite figure out how the Cauchy-Schwartz API works for the last step, but here's some help:

import Mathlib.Data.Real.Basic
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Tactic

theorem nesbitt_inequality
  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) :
  a / (b + c) + b / (c + a) + c / (a + b) ≥ 3 / 2 := by
    have hab : a + b ≠ 0 := by linarith
    have hbc : b + c ≠ 0 := by linarith
    have hca : c + a ≠ 0 := by linarith
    suffices (a / (b + c) + 1) + (b / (c + a) + 1) + (c / (a + b) + 1) ≥ 3 / 2 + 3 by linarith
    suffices (a / (b + c) + ((b + c) / (b + c))) + (b / (c + a) + ((c + a) / (c + a))) + (c / (a + b) + ((a + b) / (a + b))) ≥ 3 / 2 + 3 by
      rwa [div_self hab, div_self hbc, div_self hca] at this
    suffices (a + b + c) * ((b + c)⁻¹ + (c + a)⁻¹ + (a + b)⁻¹) ≥ 9 / 2 by
      norm_num
      rwa [div_add_div_same, div_add_div_same, div_add_div_same,
          ← add_assoc a, ← add_assoc b, ← add_assoc c,
          (by ring :  (a + b + c) / (b + c)
                    + (b + c + a) / (c + a)
                    + (c + a + b) / (a + b) =
                      (a + b + c) * ((b + c)⁻¹ + (c + a)⁻¹ + (a + b)⁻¹))]
    suffices 2 * (a + b + c) * ((b + c)⁻¹ + (c + a)⁻¹ + (a + b)⁻¹) ≥ 9 by linarith
    suffices ((b + c) + (c + a) + (a + b)) * ((b + c)⁻¹ + (c + a)⁻¹ + (a + b)⁻¹) ≥ 9 by linarith
    rw [(by norm_num : (9 : ℝ) = (1 + 1 + 1) ^ 2)]
    let x : EuclideanSpace ℝ (Fin 3) := ![(b + c), (c + a), (a + b)]
    let y : EuclideanSpace ℝ (Fin 3) := ![(b + c)⁻¹, (c + a)⁻¹, (a + b)⁻¹]
    have := real_inner_mul_inner_self_le x y
    sorry