ENNReal.ofReal less than coercion with`: ℝ≥0∞`

Stream: new members

[Austin Letson]

Hi! I am currently struggling with this proof:

import Mathlib.Data.ENNReal.Basic

open scoped ENNReal

example (s : ℤ) (D : ℕ) : ENNReal.ofReal (12 * D ^ s) ≤ (12 * D ^ s :  ℝ≥0∞) := by
  sorry

I thought it would be possible to prove using norm_cast in combination with theorems about ENNReals/NNReals, e.g., Real.toNNReal_coe, however, I have been unable to do so. I have also tried using the lift tactic.

Any pointers would be greatly appreciated!

[Eric Wieser]

Can you make things easier for yourself by using docs#ENNReal.ofNNReal here instead?

[Austin Letson]

Eric Wieser said:

Can you make things easier for yourself by using docs#ENNReal.ofNNReal here instead?

Potentially. However, I am not sure how to make that change.

I should probably give a little more context to avoid XY problem. My ENNReal.ofReal comes from edist_dist. I essentially have dist a b ≤ 12 * D ^ s and I want edist a b ≤ 12 * D ^ s. Here is an alternative MWE:

lemma foo {Space : Type} [MetricSpace Space] (s : ℤ) (D : ℕ) (pt1 pt2 : Space) (h1 : dist pt1 pt2 ≤ (12 * D ^ s : ℝ)) : edist pt1 pt2 ≤  (12 * D ^ s :  ℝ≥0∞) := by
  sorry

[Eric Wieser]

My suggestion applied to that example would be to switch from dist to nndist: but your question is still reasonable without doing so

[Austin Letson]

Okay, let me see if I can use nndist instead. Thanks!

[Kevin Buzzard]

My effort:

import Mathlib

open scoped ENNReal NNReal

example (s : ℤ) (D : ℕ) : ENNReal.ofReal (12 * D ^ s) ≤ (12 * D ^ s :  ℝ≥0∞) := by
  obtain ⟨rfl | h⟩ := eq_or_ne D 0
  · obtain ⟨rfl | h2⟩ := eq_or_ne s 0
    · simp
    · simp [zero_zpow s (by assumption)]
  · apply le_of_eq
    calc
  ENNReal.ofReal (12 * D ^ s) = ENNReal.ofNNReal (12 * D ^ s) :=
    congr_arg (ENNReal.ofNNReal) <| NNReal.coe_injective <| by
    simpa using zpow_nonneg (Nat.cast_nonneg' D) s
  _ = (12 * D ^ s :  ℝ≥0∞) := by
    push_cast
    rw [ENNReal.coe_zpow]
    · push_cast
      rfl
    · norm_cast

[Kevin Buzzard]

I have no idea why obtain ⟨rfl | h2⟩ doesn't give me a named hypothesis h2 by the way. But this is tricky in the sense that there really are different cases which need to be considered, for example 0 ^ 0 or 0 ^ -1 might behave differently. My proof goes via Eric's idea BTW.

[Kevin Buzzard]

Re the alternative: the analogue of Eric's suggestion here would be to go via nndist pt1 pt2. Did I give you enough hints? :-)

[Daniel Weber]

This is another approach, although I haven't filled in ENNReal.zpow_eq_top_iff

import Mathlib

open scoped ENNReal

lemma ENNReal.toReal_zpow (x : ℝ≥0∞) (z : ℤ) : x.toReal ^ z = (x ^ z).toReal := by
  simp [← rpow_intCast, ← toReal_rpow]

-- See note [no_index around OfNat.ofNat]
@[simp]
theorem ENNReal.ofNat_ne_top (a : ℕ) [a.AtLeastTwo] : (no_index (OfNat.ofNat a : ℝ≥0∞)) ≠ ⊤ :=
  nofun

@[simp]
theorem ENNReal.zpow_eq_top_iff (x : ℝ≥0∞) (z : ℤ) : x ^ z = ⊤ ↔ (x = ⊤ ∧ 0 < z) ∨ (x = 0 ∧ z < 0) :=
  sorry

example (s : ℤ) (D : ℕ) : ENNReal.ofReal (12 * D ^ s) ≤ (12 * D ^ s :  ℝ≥0∞) := by
  by_cases hd : D = 0 ∧ s < 0
  · simp [hd, zero_zpow _ hd.2.ne]
  · rw [← show _ = (12 * D ^ s :  ℝ≥0∞) from (ENNReal.ofReal_toReal (by simp [ENNReal.mul_eq_top, hd]))]
    simp [← ENNReal.toReal_zpow]

[Austin Letson]

Kevin Buzzard said:

I have no idea why obtain ⟨rfl | h2⟩ doesn't give me a named hypothesis h2 by the way. But this is tricky in the sense that there really are different cases which need to be considered, for example 0 ^ 0 or 0 ^ -1 might behave differently. My proof goes via Eric's idea BTW.

In my use case, I know that D < 0, however, I wasn't using this directly which I now realize gave me extra trouble.

[Austin Letson]

Thank you all! This was very helpful, both in satisfying the goal and also for my understanding of how to approach moving between ENNReal and Real.

[Yakov Pechersky]

For getting the named hypothesis, I think you have to do obtain (rfl | h2) (parens, not deconstruction)