Zulip Chat Archive

Stream: new members

Topic: AM-GM


Iocta (Apr 13 2024 at 03:58):

Am I missing out on some automation here?

theorem _sqrt_mul_le_add_div_two (a b : ) (ha : 0  a) (hb : 0  b) : Real.sqrt (a * b)  (a + b) / 2 := by
  apply sqrt_le_iff.2
  rw [div_pow]
  norm_num
  rw [pow_two, add_mul, mul_add, mul_add, add_assoc, mul_comm b a, add_assoc (a * a),]
  apply And.intro
  sorry
  have : 0  a * b * 2 + a ^ 2 + b ^ 2 - 4 * a * b
  {
    ring_nf
    rw [add_comm, add_assoc, mul_comm, mul_assoc, ]
    sorry
  }

Johan Commelin (Apr 13 2024 at 04:01):

I didnt test, but can ring_nf; nlinarith solve this after line 1?

Johan Commelin (Apr 13 2024 at 04:01):

Maybe throw in a field_simp for good measure

Iocta (Apr 13 2024 at 04:02):

nlinarith fails

Johan Commelin (Apr 13 2024 at 04:15):

import Mathlib

theorem _sqrt_mul_le_add_div_two (a b : ) (ha : 0  a) (hb : 0  b) : Real.sqrt (a * b)  (a + b) / 2 := by
  apply Real.sqrt_le_iff.2
  field_simp
  ring_nf
  suffices a * b * 2  a ^ 2 + b ^ 2 by constructor <;> linarith
  have : 0  (a - b) ^ 2 := by nlinarith
  nlinarith

David Renshaw (Apr 13 2024 at 15:33):

note that mathlib has docs#Real.geom_mean_le_arith_mean2_weighted

Heather Macbeth (Apr 13 2024 at 20:37):

The first part of Johan's proof is psychologically useful but not actually necessary.

theorem _sqrt_mul_le_add_div_two (a b : ) (ha : 0  a) (hb : 0  b) : Real.sqrt (a * b)  (a + b) / 2 := by
  apply Real.sqrt_le_iff.2
  have : 0  (a - b) ^ 2 := by positivity
  constructor <;> linarith

Eric Wieser (Apr 13 2024 at 21:14):

Should this lemma be in mathlib? And if so, do we want the 3-ary version too?

Heather Macbeth (Apr 13 2024 at 22:08):

I happened to prepare the 3-ary version recently for a talk!

import Mathlib

example (a b c : ) (ha : 0  a) (hb : 0  b) (hc : 0  c) :
    (a * b * c) ^ ((3:)⁻¹)  (a + b + c) / 3 := by
  rw [Real.rpow_inv_le_iff_of_pos]
  · norm_cast
    have : 0  (a + b + c) * ((b - c) ^ 2 + (a - b) ^ 2 + (c - a) ^ 2) := by positivity
    have : 0  a * (b - c) ^ 2 + c * (a - b) ^ 2 + b * (c - a) ^ 2 := by positivity
    linarith
  all_goals positivity

The 2-ary version seems reasonable to be in mathlib (since sqrt is a named special operation), the others don't seem like obvious inclusions to me given that the n-ary one exists.

Iocta (Apr 13 2024 at 22:28):

Is this w in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/MeanInequalities.html#Real.geom_mean_le_arith_mean typical in the statement of this theorem or definition? I don't see it in https://en.wikipedia.org/wiki/Geometric_mean (I guess w i = 1)


Last updated: May 02 2025 at 03:31 UTC