Tactics for NNREAL

Stream: new members

[Yunong Shi]

As a practice, I am trying to prove the arithmetic mean geometric mean inequality of 2 positive real numbers.

I tried to prove the \R and NNREAL (non-negative real) version respectively. I find that many tactics, including linarith and ring doesn't work for NNREAL but works for \R. I am wondering why this is the case? I looked it up and NNREAL is just def nnreal := {r: real // r >= 0}

Here are the codes, as shown, I could not use linarith for the nnreal case.

real version:

theorem amgm : ∀ x y: ℝ, 4 * x * y ≤ (x + y) * (x + y) := by
  intro x y
  let z:= x - y
  calc
      4 * x * y ≤ z * z + 4 * x * y := by linarith [mul_self_nonneg z]
      _ ≤ (x - y) * (x - y) + 4 * x * y  := by simp [z]
      _ = (x + y) * (x + y) := by linarith

nnreal version

theorem AMGM :  ∀ x y: NNReal, NNReal.sqrt (x * y) ≤  (x + y)/2 := by
  intro x y
  have sq_amgm: 4 * x * y ≤ (x + y) * (x + y) :=
    let z:= x - y
    calc
      4 * x * y ≤ z * z + 4 * x * y := by   -- cannot use linarith here.
        have z_sq_pos: 0 ≤ z * z := by
          simp [z, mul_self_nonneg]
        apply le_add_of_nonneg_left z_sq_pos
      _ ≤ (x - y) * (x - y) +  4 * x * y := by simp [z]
      _ = x * x - x * y - y * x + y * y +  4 * x * y := by sorry -- cannot use linarith here.

[Eric Wieser]

This works:

      4 * x * y ≤ z * z + 4 * x * y := by
        rw [←NNReal.coe_le_coe]
        push_cast
        nlinarith

[Yunong Shi]

Eric Wieser said:

This works:

      4 * x * y ≤ z * z + 4 * x * y := by
        rw [←NNReal.coe_le_coe]
        push_cast
        nlinarith

Thanks! @Eric Wieser . What about the last line (with sorry)?

On a high-level, why do I need to use different tactics for NNReal and R? and how do I find out which tactics that I can use with NNReal?

[Patrick Massot]

The main issue is that NNReal is not a field (or even a ring).

[Yunong Shi]

Patrick Massot said:

The main issue is that NNReal is not a field (or even a ring).

Got it, makes sense! Probably I'd better off use Real together with x >= 0 rather than NReal I assume.

[Eric Wieser]

NNReal is often the better choice; just know how to convert back to real mid-proof when you need to

[Eric Wieser]

(Which I did above with a suitable rw and push_cast)

[Patrick Massot]

Honestly I'm not so convinced that NNReal is often the better choice. I spent a lot of time last week helping students suffering with this and the gain wasn't clear at all. And it was a nightmare in LTE.

[Eric Wieser]

The main advantage of NNReal is that it saves you from getting the same side goals about positivity over and over again

[Eric Wieser]

And it's often convenient to have OrderBot when working with iSup

[Kevin Buzzard]

Yeah but we have positivity now.

[Yaël Dillies]

No, it is still quite a pain in simp and simp_rw