help plsssss amgm

Stream: mathlib4

[annie yuan 🐟]

hi, I am a struggling student desperately seeking help proving this hypothesis using the amgm inequality

-- (a + b)/2 ≥ (ab).sqrt
-- a and b previously defined as positive and real
have hab : (a + b) / 2 ≥ (a * b) ^ (1/2) := by
sorry

[Ruben Van de Velde]

A #mwe could be helpful. Are you specifically asking about the relation between Real.sqrt x and x ^ (1/ 2)?

[Floris van Doorn]

docs#two_mul_le_add_sq is a version of AM-GM, but not quite in the form you want.