AM inequality in the form 4 * a * b ≤ (a + b) ^ 2

Stream: Is there code for X?

[Christoph Spiegel]

I am looking for the binary arithmetic-geometric-mean inequality in the form 4 * a * b ≤ (a + b) ^ 2. two_mul_le_add_sq in Algebra.Order.Ring.Unbundled.Basicgives 2 * a * b ≤ a ^ 2 + b ^ 2 and if one is e.g. in Nat then linarith let's one easily get from the latter to the former. Is there a reason why the former isn't its own result four_mul_le_add_sq? I tried implementing it in Algebra.Order.Ring.Unbundled.Basic, but one would (probably?) need [CommSemiring α] which apparently conflicts with [ExistsAddOfLE α].

[Yaël Dillies]

Where did you get that it conflicts?

[Christoph Spiegel]

Ah, it appears that [CommSemiring α] needs to be specified prior to [ExistsAddOfLE α] in the arguments. Is this known / expected behavior?

[Ruben Van de Velde]

Sounds expected, you need an addition

[Christoph Spiegel]

Nevermind, [CommSemiring α] was already previously declared so the issue was probably re-declaring it.

[Christoph Spiegel]

Anyone see a more direct way to prove this? #17877

[Jireh Loreaux]

I'm not sure if it would be bad to import Mathlib.Tactic.Ring here (@Yaël Dillies do you know?), but if it were reasonable then:

import Mathlib.Algebra.Order.Ring.Unbundled.Basic
import Mathlib.Tactic.Ring

lemma four_mul_le_add_sq [CommSemiring α] [LinearOrder α] [ExistsAddOfLE α] [MulPosStrictMono α]
    [ContravariantClass α α (· + ·) (· ≤ ·)] [CovariantClass α α (· + ·) (· ≤ ·)]
    (a b : α) : 4 * a * b ≤ (a + b) ^ 2 := by
  calc 4 * a * b
    _ = 2 * a * b + 2 * a * b := by ring
    _ ≤ a ^ 2 + b ^ 2 + 2 * a * b := by gcongr; exact two_mul_le_add_sq _ _
    _ = (a + b) ^ 2 := by ring

[Yaël Dillies]

Yes, it's quite bad to import ring here

[Christoph Spiegel]

I think doing it in Mathlib.Algebra.Order.Ring.Unbundled.Basic causes an import cycle:

stderr:
✖ [324/614] Running Mathlib.Algebra.Order.Ring.Unbundled.Basic
error: build cycle detected:
  +Mathlib.Tactic.Ring:olean
  +Mathlib.Algebra.Order.Ring.Unbundled.Basic:deps
  +Mathlib.Algebra.Order.Ring.Unbundled.Basic:leanArts
  +Mathlib.Algebra.Order.Ring.Unbundled.Basic:olean
  +Mathlib.Algebra.Order.Ring.Defs:deps
  +Mathlib.Algebra.Order.Ring.Defs:leanArts
  +Mathlib.Algebra.Order.Ring.Defs:olean
  +Mathlib.Algebra.Order.Ring.Rat:deps
  +Mathlib.Algebra.Order.Ring.Rat:leanArts
  +Mathlib.Algebra.Order.Ring.Rat:olean
  +Mathlib.Tactic.Ring.Basic:deps
  +Mathlib.Tactic.Ring.Basic:leanArts
  +Mathlib.Tactic.Ring.Basic:olean
  +Mathlib.Tactic.Ring:deps
  +Mathlib.Tactic.Ring:leanArts
  +Mathlib.Tactic.Ring:olean

But the lemma could presumably be stated and proven with ring elsewhere. I'm not even sure why two_mul_le_add_sq is there in the first place. Is it really that "basic" of a statement for ordered (semi)rings? A quick search of mathlib only shows one use in the Finset CS inequality and another in L2Spaces.

[Kevin Buzzard]

two_mul_le_add_sq feels more basic to me than four_mul_le_add_sq (which should probably be four_mul_le_sq_add?) because in a semiring you can't subtract. For example Jireh has shown how to prove your result from mathlib's -- how will you prove mathlib's from your result? Edit: hmm, maybe that's what the ContravariantClass assumption does?

[Christoph Spiegel]

two_mul_le_add_sq is more basic and #17877 doesn't try to replace it or move it (it also derives four_mul_le_sq_add from it). But to me it's also not really a binary (division-free) version of the AM GM inequality as the documentation suggests. If four_mul_le_sq_add is more at home in some other file (where we can also import ring), I'm happy to move it there and simplify the proof like @Jireh Loreaux suggested. But I think if people look for a division-free binary AM GM inequality (as we did), this is what they should find.

[Christoph Spiegel]

@Kevin Buzzard Actually ContravariantClass is also an assumption of two_mul_le_add_sq, so they do seem to be equivalent (quick and dirty proof):

example [ExistsAddOfLE α] [MulPosStrictMono α]
    [ContravariantClass α α (· + ·) (· ≤ ·)] [CovariantClass α α (· + ·) (· ≤ ·)]
    (a b : α) : 2 * a * b ≤ a ^ 2 + b ^ 2 := by

    have := calc 2 * a * b + 2 * a * b
      _ =  2 * (a * b) + 2 * (a * b) := by simp [NonUnitalSemiring.mul_assoc]
      _ = (2 + 2) * (a * b) := Eq.symm (RightDistribClass.right_distrib 2 2 (a * b))
      _ = 4 * (a * b) := by rw [two_add_two_eq_four]
      _ = 4 * a * b := Eq.symm (mul_assoc 4 a b)
      _ ≤ (a + b) ^ 2 := four_mul_le_add_sq a b
      _ = a ^2 + 2 * a * b + b ^ 2 := add_pow_two a b
      _ = a ^ 2 + b ^ 2 + 2 * a * b := add_right_comm (a ^ 2) (2 * a * b) (b ^ 2)

    exact (add_le_add_iff_right (2 * a * b)).mp this

[Christoph Spiegel]

Guess that reaffirms my opinion that neither of these results belongs in this file?

[Jireh Loreaux]

I'm not sure why you say neither of these results belongs in this file? This seems like the appropriate place, unbundled ordered rings.

[Christoph Spiegel]

Less of a mathematical distinction and more of a programming one: the import loop for ring seems to imply that this file contains base properties of rings. Any higher level results that (1) one would expect to be explicitly pointed out in a proof and (2) would be much easier to prove in mathlib with access to ring feel like they should not be part of the imports needed to make ring work? But I may be completely off about how ring is constructed and am also not really familiar with the algebraic side of mathlib.

[Christoph Spiegel]

But regardless, the main point is that two_mul_le_add_sq to me isn't quite a division-free binary AM GM inequality :big_smile:

[3sh V]

Hi, I am trying to import Algebra.Order.Ring.Unbundled.Basic``
I get "unknown module prefix 'Algebra'". Do I need to add some requires in lakefile.toml?

Oh sorry,I figured out. Its

import Mathlib.Algebra.Order.Ring.Unbundled.Basic

:D