Schur's Inequality

Stream: Is there code for X?

[Sabbir Rahman]

Is there Schur's inequality in mathlib. I did search through leansearch, but didn’t find it. So my guess is it isn’t, but want to be sure.

[Sabbir Rahman]

Also proving it seems to be a bit annoying. To follow the standard proof, I guess one has to use wlog but doing casework to make up all sorted orders of three variables is painful. Sometimes I wish, there was tactic to state largest variable or assign an order to variables using wlog.

[Luigi Massacci]

Modulo that I'm not an expert, but I think you can just write down the six cases, then each is a single calc line by ring followed by exact ordered_case I think, which is not too painful. I always find wlog to be more of a distraction since it doesn't really match what people mean on paper.

[Bhavik Mehta]

import Mathlib.Analysis.SpecialFunctions.Pow.Real

lemma schur {a b c r : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hr : 0 < r) :
    0 ≤ a ^ r * (a - b) * (a - c) + b ^ r * (b - a) * (b - c) + c ^ r * (c - a) * (c - b) := by
  wlog hcb : c ≤ b generalizing a b c
  case inr => linarith [this ha hc hb (by linarith)]
  wlog hba : b ≤ a generalizing a b c
  case inr =>
    rcases le_total a c with hac | hca
    case inl => linarith [this hb hc ha hac hcb]
    case inr => linarith [this hb ha hc hca (by linarith)]
  have hcr : 0 ≤ c ^ r := Real.rpow_nonneg hc r
  have h₁ : 0 ≤ c ^ r * (c - a) * (c - b) := by
    rw [mul_assoc]
    exact mul_nonneg hcr (by nlinarith)
  have he : a ^ r * (a - b) * (a - c) + b ^ r * (b - a) * (b - c) =
      (a - b) * (a ^ r * (a - c) - b ^ r * (b - c)) := by
    ring
  rw [he]
  refine add_nonneg ?_ h₁
  refine mul_nonneg (by linarith) ?_
  rw [sub_nonneg]
  gcongr ?_ ^ _ * (?_ - _)
  linarith

[Bhavik Mehta]

Sabbir Rahman said:

Sometimes I wish, there was tactic to state largest variable or assign an order to variables using wlog.

I agree with this part though

[Sabbir Rahman]

Nice, I hadn't thought of doing wlog two times, that does make the proof much more nicer

[Sabbir Rahman]

Luigi Massacci said:

Modulo that I'm not an expert, but I think you can just write down the six cases, then each is a single calc line by ring followed by exact ordered_case I think, which is not too painful. I always find wlog to be more of a distraction since it doesn't really match what people mean on paper.

wlog certainly doesn't match what we do in informal proofs, but I have gotten used to it

[Bhavik Mehta]

I've put this inequality (generalised to 0 <= r) and a bunch of other generalisations in the PR #24618.

[Bhavik Mehta]

In fact, we can make linear_combination do massive chunks of the proofs:

lemma vornicu_schur_mildorf {α : Type*} [PartialOrder α] [CommRing α] [IsOrderedRing α]
    {a b c x y z : α}
    (hx : 0 ≤ x) (hz : 0 ≤ z) (hcb : c ≤ b) (hba : b ≤ a) (hyxz : y ≤ x + z) :
    0 ≤ x * (a - b) * (a - c) + y * (b - a) * (b - c) + z * (c - a) * (c - b) := by
  have h₁ : 0 ≤ a - b := by linear_combination hba
  have h₂ : 0 ≤ b - c := by linear_combination hcb
  linear_combination h₁ * x * (a - b) + h₂ * z * (b - c) + hyxz * (b - c) * (a - b)

lemma schur {a b c r : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hr : 0 ≤ r) :
    0 ≤ a ^ r * (a - b) * (a - c) + b ^ r * (b - a) * (b - c) + c ^ r * (c - a) * (c - b) := by
  wlog hcb : c ≤ b generalizing a b c
  next => linear_combination this ha hc hb (le_of_not_le hcb)
  wlog hba : b ≤ a generalizing a b c
  next =>
    obtain hac | hca := le_total a c
    case inl => linear_combination this hb hc ha hac hcb
    case inr => linear_combination this hb ha hc hca (le_of_not_le hba)
  refine vornicu_schur_mildorf (Real.rpow_nonneg ha _) (Real.rpow_nonneg hc _) hcb hba ?_
  linear_combination Real.rpow_le_rpow hb hba hr + Real.rpow_nonneg hc r