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