AM-GM

Stream: Is there code for X?

[Yaël Dillies]

Do we really not have the plain vanilla less-variables-becomes-trivial AM-GM?

lemma two_mul_sqrt_le_add {x y : ℝ} (h : 0 ≤ x + y) :
  2 * sqrt (x * y) ≤ x + y :=

[Kevin Buzzard]

Is this OK for e.g. x=+1, y=-1? I don't know what Lean thinks real.sqrt(-1) is...

[Yaël Dillies]

I read the docstring before writing wrong stuff for once :upside_down: :
"The square root of a real number. This returns 0 for negative inputs."

[Martin Dvořák]

OT about the real.sqrt of negative numbers... We should never be able to prove (sqrt x = sqrt y) → (x = y) right?

[Eric Wieser]

We can for nnreal

[Martin Dvořák]

How lovely we can guarantee non-negativity by a TYPE.