How does one show 0 < ![1 / 3, 1 / 3, 1 / 3]?

Stream: new members

[Janitha Aswedige]

I'm trying to use the am-gm inequality using "theorem geom_mean_le_arith_mean". And I got

⊢ 0 < ![1 / 3, 1 / 3, 1 / 3]

as one of the goals. How do I prove this?

[David Renshaw]

something like ext i; fin_cases i <;> norm_num should work

[David Renshaw]

if there's a better way, I'd be eager to hear about it

[Ruben Van de Velde]

No, that sounds great

[Janitha Aswedige]

ext i gives the following message ; applyExtTheorem only applies to equations, not
0 ≤ ![1 / 3, 1 / 3, 1 / 3] ∧ ¬![1 / 3, 1 / 3, 1 / 3] ≤ 0

[Jireh Loreaux]

I think you want

apply lt_of_strongLT fun i ↦ ?_
fin_cases i
norm_num

(untested though)

[David Renshaw]

import Mathlib

example : 0 < ![(1/3 : ℚ), 1/3, 1/3] := by
  apply lt_of_strongLT fun i ↦ ?_
  fin_cases i <;> norm_num