norm_num not solving ennreal power goals

Stream: new members

[Julian Berman]

Can someone give us a hint on:

import Mathlib.Data.ENNReal.Basic
open ENNReal
lemma bar : (6 : ℝ≥0∞) * 2 ^ (-2 : ℤ) ≤ 2 := sorry

[Edward van de Meent]

there you go

Solution

import Mathlib.Data.ENNReal.Inv
open ENNReal

lemma bar : (6 : ℝ≥0∞) * 2 ^ (-2 : ℤ) ≤ 2 := by
  have h1 : (2:ℝ≥0∞) ≠ 0 := by norm_num
  have h2 : (2:ℝ≥0∞) ≠ ⊤ := by norm_num
  calc
    (6:ℝ≥0∞) * 2 ^ (-2:ℤ)
      = 6 * (2 ^ 2)⁻¹ := by
        rfl
    _ = 6 * (2 * 2)⁻¹ := by
      rw [pow_two]
    _ = 3 * 2 * (2⁻¹ * 2⁻¹) := by
      rw [ENNReal.mul_inv (Or.inl h1) (Or.inl h2)]
      norm_num
    _ ≤ 2 := by
      rw [mul_assoc]
      rw [← mul_assoc 2,ENNReal.mul_inv_cancel h1 h2,one_mul]
      rw [ENNReal.mul_inv_le_iff h1 h2]
      norm_num

[Edward van de Meent]

something that helps is importing more than just ENNReal.Basic.

[Eric Wieser]

Ennreal isn't a semi field, so even if I finish my PR for norm_num on NNReal and NNRat, it won't help here

[Julian Berman]

I guess that proof shows we were sort of on the right track but I thought "surely it can't be that long / manual" and kept restarting from the top. EDIT: and thanks obviously!

[Edward van de Meent]

there possibly is a way to do this by first showing that it suffices to show this for NNReal, then using norm_num, but i didn't really feel like dealing with the casts

[Kevin Buzzard]

unfortunately even have bar : (6 : ℝ≥0) * 2 ^ (-2 : ℤ) ≤ 2 := by norm_num seems to fail

[Julian Berman]

We were trying to do that but by lifting to \R even -- is that at all a feasible route?

[Edward van de Meent]

i think so? it's just a question of if it's worth the hassle

[Kevin Buzzard]

It seems to me that there might be a bunch of missing lemmas (or lemmas not tagged norm_cast or something?). I would have expected this to reduce the question to ℝ≥0but it doesn't, for some reason:

import Mathlib.Data.ENNReal.Basic

open ENNReal

open NNReal

lemma bar : (6 : ℝ≥0∞) * 2 ^ (-2 : ℤ) ≤ 2 := by
  change ((6 : ℝ≥0) : ℝ≥0∞) * (2 : ℝ≥0) ^ (-2 : ℤ) ≤ (2 : ℝ≥0) -- works great
  -- ⊢ ↑6 * ↑2 ^ (-2) ≤ ↑2
  norm_cast -- cast away those norms and leave us with an ℝ≥0 goal please
  -- ⊢ 6 * 2 ^ Int.negSucc 1 ≤ 2 -- looks good
  -- until you discover that (6 : ℝ≥0∞) :-/
  sorry

[Julian Berman]

lemma baz : (2 : ℝ≥0∞) ^ (-1 : ℤ) ≤ 1 := by norm_num -- fails

was also surprising

[Ruben Van de Velde]

import Mathlib

open NNReal ENNReal

lemma x2 {n : ℕ} [hn : n.AtLeastTwo] {x : ENNReal} : x ^ (- (OfNat.ofNat n : ℤ)) = (x ^ OfNat.ofNat n)⁻¹ := by
  apply zpow_neg_coe_of_pos
  have := hn.one_lt
  omega

lemma bar : (6 : ℝ≥0∞) * 2 ^ (-2 : ℤ) ≤ 2 := by
  rw [x2]
  simp_rw [← ENNReal.coe_ofNat]
  norm_num
  simp_rw [← ENNReal.coe_ofNat]
  rw [← ENNReal.coe_inv (by norm_num)]
  rw [← ENNReal.coe_mul]
  rw [ENNReal.coe_le_coe]

  simp_rw [← Real.toNNReal_ofNat]
  rw [← Real.toNNReal_inv, ← Real.toNNReal_mul (by norm_num)]
  rw [@Real.toNNReal_le_toNNReal_iff']
  norm_num

:/

[Edward van de Meent]

my guess would be that the exponent is to blame?

[Kevin Buzzard]

import Mathlib.Data.ENNReal.Inv

open ENNReal

open NNReal

lemma bar : (6 : ℝ≥0∞) * 2 ^ (-2 : ℤ) ≤ 2 := by
  change ((6 : ℝ≥0) : ℝ≥0∞) * (2 : ℝ≥0) ^ (-2 : ℤ) ≤ (2 : ℝ≥0) -- works great
  rw [← ENNReal.coe_zpow (show (2 : ℝ≥0) ≠ 0 by norm_num)] -- norm_cast can't do this
  norm_cast
  -- ⊢ 6 * 2 ^ Int.negSucc 1 ≤ 2 -- now NNReal
  rw [← NNReal.coe_le_coe]
  norm_num

[Kevin Buzzard]

docs#ENNReal.coe_zpow is tagged norm_cast but need a hypothesis r ≠ 0. Does this mean that it will never fire?

[Austin Letson]

We looked at coe_zpow but thought because it was tagged with simp and norm_cast it wasn't working. Thank you all!