AM-GM

Stream: new members

[Iocta]

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]

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

[Johan Commelin]

Maybe throw in a field_simp for good measure

[Iocta]

nlinarith fails

[Johan Commelin]

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]

note that mathlib has docs#Real.geom_mean_le_arith_mean2_weighted

[Heather Macbeth]

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]

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

[Heather Macbeth]

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]

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)