converting between reals, ENNReals and Nats

Stream: new members

[Becker A.]

I keep having to close proofs that would be trivial in Nat's but feels non-trivial because some of the numbers involved are Nat literals casted to Reals or ENNReals.

below are just a couple that I can think of atm:

import Mathlib.Analysis.Normed.Group.Basic
import Mathlib.MeasureTheory.MeasurableSpace.Defs
import Mathlib.MeasureTheory.Measure.MeasureSpaceDef
import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
import Mathlib.Probability.Independence.Basic
import Mathlib.Probability.Moments.Basic
import Mathlib.MeasureTheory.Function.L1Space.Integrable
import Mathlib.Data.Finset.Range

open scoped ENNReal


theorem memLp_pow.extracted_1_1
  (n m : ℕ)
  (x : ℝ)
  : x ^ (OfNat.ofNat 2 * ↑m) = x ^ (2 * m)
  := by
  sorry

theorem moment_2_biased_svar.extracted_1_3
  : (@OfNat.ofNat ℝ≥0∞ 2 instOfNatAtLeastTwo) * (@OfNat.ofNat ℝ≥0∞ 2 instOfNatAtLeastTwo)
    = OfNat.ofNat 4
  := by
  sorry

please advise, thanks!

[Ilmārs Cīrulis]

import Mathlib.Data.ENNReal.Basic

open scoped ENNReal

theorem memLp_pow.extracted_1_1
    (n m : ℕ) (x : ℝ) : x ^ (OfNat.ofNat 2 * ↑m) = x ^ (2 * m) := by
  rfl

theorem moment_2_biased_svar.extracted_1_3 :
    (@OfNat.ofNat ℝ≥0∞ 2 instOfNatAtLeastTwo) *
    (@OfNat.ofNat ℝ≥0∞ 2 instOfNatAtLeastTwo) = OfNat.ofNat 4 := by
  grind

[Kevin Buzzard]

I'm surprised you're seeing OfNat.ofNat 2 ever: how did those appear? What was the line you wrote that made them show up?

[Becker A.]

@Kevin Buzzard it was this (I feel bad for not reducing but it's not too long):

import Mathlib.Analysis.Normed.Group.Basic
import Mathlib.MeasureTheory.MeasurableSpace.Defs
import Mathlib.MeasureTheory.Measure.MeasureSpaceDef
import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
import Mathlib.Probability.Independence.Basic
import Mathlib.Probability.Moments.Basic
import Mathlib.MeasureTheory.Function.L1Space.Integrable
import Mathlib.Data.Finset.Range

open Finset MeasureTheory ProbabilityTheory NNReal
open scoped ENNReal


theorem memLp_pow
  (Ω : Type u_1) [MeasurableSpace Ω]
  (n m : ℕ)
  (f : Ω → ℝ)
  (P : Measure Ω) [IsProbabilityMeasure P]
  (hFMemLp : MemLp f ((2 * m) * n) P)
  : MemLp (f ^ (2 * m)) n P
  := by
  have hFFun : f ^ (2 * m) = fun ω => f ω ^ (2 * m) := by rfl
  conv in (f ^ (2 * m)) => rw [hFFun]
  conv in (_ ^ (2 * m)) => rw [pow_mul, <- sq_abs, <- Real.norm_eq_abs, <- pow_mul]
  have h1 :=  MemLp.norm_rpow_div (f := f) (q := (2 * m)) (hFMemLp)
  have h2 : ∀ x : ℝ, x ^ (@OfNat.ofNat ℝ 2 instOfNatAtLeastTwo * ↑m) = x ^ (2 * m) := by
    sorry
  conv at h1 in (_ ^ (2 * _).toReal) =>
    rw [ENNReal.toReal_mul, ENNReal.toReal_ofNat, ENNReal.toReal_natCast, h2]
  conv at h1 in (_ / _) => rw [mul_comm, <- mul_div]
  sorry

[Becker A.]

it showed up around the sorry's; specifically I'm trying to use MemLp.norm_rpow_div and it involves doing division of Nat's casted to Reals and ENNReals (I may have written the original problem wrong, but this is the source so this should be representative of what I actually need)

[Kevin Buzzard]

Wait, so the horrible ofNats (which a user should never see) are literally introduced by you in h2? What is the role of h2 here? You never use it?

[Becker A.]

I use it on the third to last line... I just copied my tactic state into a have so I could solve it in an isolated context

[Becker A.]

the tactic state showed ofNat, I didn't intentionally reach for it it's just what I was presented to solve by mathlib

[Kevin Buzzard]

Right, so what I am asking you is what you typed to make the ofNat appear, because it wasn't in your goal to start with, and it was in your goal at some point, so something you did made it appear.

[Kevin Buzzard]

theorem memLp_pow
    (Ω : Type*) [MeasurableSpace Ω]
    (n m : ℕ)
    (f : Ω → ℝ)
    (P : Measure Ω) [IsProbabilityMeasure P]
    (hFMemLp : MemLp f ((2 * m) * n) P) :
    MemLp (f ^ (2 * m)) n P := by
  have hFFun : f ^ (2 * m) = fun ω => f ω ^ (2 * m) := by rfl
  conv in (f ^ (2 * m)) => rw [hFFun]
  conv in (_ ^ (2 * m)) => rw [pow_mul, <- sq_abs, <- Real.norm_eq_abs, <- pow_mul]
  have h1 :=  MemLp.norm_rpow_div (f := f) (q := (2 * m)) (hFMemLp)
  -- I didn't read any of the above but here's my instinct on what to do next
  convert h1
  · rw [← Real.rpow_natCast]
    congr
    norm_num
  · -- goal looks problematic because you've divided by something which might be zero
    sorry

[Becker A.]

Kevin Buzzard said:

Right, so what I am asking you is what you typed to make the ofNat appear, because it wasn't in your goal to start with, and it was in your goal at some point, so something you did made it appear.

I hovered over the infoview tactic state to know what to copy into h2, and the infoview gave me ofNat

[Kevin Buzzard]

Let's talk about h1 before h2: you have divided by 2m. Do you know that 2m isn't zero?

[Becker A.]

yeah; I can switch that to (2 * (m + 1)) and it'll still be useful

[Kevin Buzzard]

You shouldn't be using lots of lemmas: there are tools like norm_num which should be doing all the work for you. See for example how I solved the first goal.

[Becker A.]

okay, is there any way I would I know about stuff like norm_num on my own? it seems like most solutions to my questions use tactics that I just don't know exist (e.g., grind or norm_num), so that alone might fix a lot of my problems

[Kevin Buzzard]

  -- I didn't read any of the above but here's my instinct on what to do next
  convert h1 -- because modulo stupid issues with nat v ennreal the goal is solved by h1
  -- now pick up the pieces
  · rw [← Real.rpow_natCast] -- change x^natural to x^(coerced to real)
    simp
  · norm_cast
    rw [ENNReal.eq_div_iff] -- clear denominators
    · norm_cast
    · sorry -- impossible
    · exact?

[Kevin Buzzard]

I found Real.rpow_natCast by writing the lemma I wanted

example (x : ℝ) (n : ℕ) : x ^ (n : ℝ) = x ^ n := by exact?

and using exact?, and similarly I found the last lemma in my proof using exact? (and left the exact? there). norm_num and norm_cast are useful tactics in this situation; there are only a small number of useful tactics and it's just worth picking them up and then hovering over them to read their docstrings. push_cast is another one. I found ENNReal.eq_div_iff by guessing the name but usually I find lemmas using exact? -- there are hundreds of thousands of lemmas so it's hopeless learning them all, but learning the relevant tactics for your area is definitely a doable thing.

[Becker A.]

wait do the dots automatically enter you into generated cases? I thought you had to do case NAME => every time

[Kevin Buzzard]

After the rewrite I had three goals (because the rewrite only worked under some assumptions) so I just wrote \. sorry and then cut and pasted it three times

[Becker A.]

yeahhh I kept trying to use div_eq_iff instead of ENNReal.eq_div_iff and didn't know why it didn't work :\ also I replaced it with exact? and that failed, then I tried rw? and that was overwhelming.

-> searching lemmas is hard T-T

[Becker A.]

ohhh you set aside the lemma and then use exact?, got it

[Kevin Buzzard]

yeah there are lots of ways to search, there is loogle and there are semantic search engines like https://leandex.projectnumina.ai/ but sometimes when you know the lemma will be there and you're pretty sure you know the exact form, exact? is the easiest approach (and works without internet).

div_eq_iff, if you #check it, you'll see it works for GroupWithZeros, so it would work for $\mathbb{R}$ and $\mathbb{R}_{\geq0}$ (both of which are multiplicative groups if you remove the zero) but not for ENNReal (which isn't, because infinity is problematic). In situations like this it's often best to search for the analogous lemma but in the relevant namespace, because then you'll get a version which works for the bespoke type possibly with extra assumptions (e.g. I had to not only prove that something wasn't 0, but also that it wasn't infinity, here).

[Becker A.]

so in general: instead of going to the infoview and copying stuff like ofNat, it's better to use expressions with coercion like 2 : Real?

[Becker A.]

also small style question: is there a well-accepted preference when specifying nonzero nats to use
(n : Nat) (hn : n ≠ 0) : n ...
or
(n : Nat) : (n + 1) ...?

i.e., provide an explicit proof of non-zero, or just use (n + 1) instead?

[Aaron Liu]

If you have n - 1 in the statement for n nonzero then usually it's a good idea to replace n with n + 1