Performing arithmetic with ENNReals

Stream: new members

[Robert Shlyakhtenko]

I am working with the PMF defined in Mathlib.Probability.ProbabilityMassFunction.Basic as:

def PMF.{u} (α : Type u) : Type u := { f : α → ℝ≥0∞ // HasSum f 1 }

This involves a function into the extended non-negative reals. Currently, I don't need to work with infinity; every real number I am dealing with is finite.

A lot of basic arithmetic statements that would be easy to prove seem to require a lot more effort when the objects involved are typed as extended non-negative reals. For instance, this lemma is handled "by ring:"

lemma test (lmd : Real): 1/2 + 1/2 + lmd - lmd = 1/2 + lmd + (1/2 - lmd) := by ring

But this statement is not:

have h1: (2⁻¹ : ENNReal) + 2⁻¹ + ↑lmd - ↑lmd = 2⁻¹ + ↑lmd + (2⁻¹ - ↑lmd) := by sorry

(In the above statement, lmd is a NNReal less than or equal to 1/2.)

Is there an easy way to get Lean to deal with the coercions into the extended non-negative reals? After reading this stack exchange answer, I tried "norm_cast" (together with "lift"), but couldn't find a way to get it to work.

Thanks a lot!

[Aaron Liu]

That seems like a bad definition

[Bolton Bailey]

Yes, I feel like I noticed this too recently

#Is there code for X? > Statistical distance for `PMF`s? @ 💬

[Bolton Bailey]

I feel at the very least, wrt
FunLike (PMF α) α ℝ≥0∞
We could have additionally/instead:
FunLike (PMF α) α ℝ≥0

[Etienne Marion]

You can't have two FunLike instances. Finite measures are indeed coerced as functions taking values in NNReal (MeasureTheory.FiniteMeasure.instFunLike). On the same idea there is also docs#MeasureTheory.Measure.real.

[Aaron Liu]

How about make a function that takes a f : α → ℝ≥0 along with a proof of HasSum f 1 and returns a PMF α

[Devon Tuma]

This was change awhile back to make manipulating tsums easier without needing to show convergence and to align PMF.toOuterMeasure with the ENNReal in OuterMeasure.measureOf, but that did make more basic arithmetic difficult in a lot of cases

[Eric Wieser]

Robert Shlyakhtenko said:

But this statement is not [provable by ring]

have h1: (2⁻¹ : ENNReal) + 2⁻¹ + ↑lmd - ↑lmd = 2⁻¹ + ↑lmd + (2⁻¹ - ↑lmd) := by sorry

(In the above statement, lmd is a NNReal less than or equal to 1/2.)

This needs #9915

[Peter Hansen]

Maybe field_simp is worth a mention:

example (lmd : NNReal) (h : lmd ≤  (1 / 2 : ENNReal))  : (2⁻¹ : ENNReal) + 2⁻¹ + ↑lmd - ↑lmd = 2⁻¹ + ↑lmd + (2⁻¹ - ↑lmd) := by
  field_simp

[Robert Shlyakhtenko]

Thanks a lot for the helpful responses! Too bad that #9915 has not been merged yet.

[Aaron Liu]

I hope #9915 gets merged soon

[Bryan Gin-ge Chen]

Is it even ready for review? The draft status and please-adopt / WIP tags suggest otherwise...

[Aaron Liu]

I don't know, I worked on it a bit and I got CI succeeding

[Bryan Gin-ge Chen]

I've only just skimmed it but it seems reasonably ready for review, so I've removed the WIP and please-adopt tags and removed the draft status as well. In return, do you mind "taking over" the PR? I guess you might have to migrate it to a branch on your fork at some point though.

[Aaron Liu]

I don't know how to do that

[Bryan Gin-ge Chen]

Migrating a branch to a fork? scripts/migrate_to_fork.py can do it for you, but don't worry about too much about it for now. Let's see if someone reviews the PR first.

[Aaron Liu]

But I'm not the person who created the PR, I don't know if that will cause problems

[Bryan Gin-ge Chen]

If the script doesn’t work, we can walk you through doing it manually. (Ultimately it’s just pushing a copy of the branch to your fork and opening a new PR from there)

[Robert Shlyakhtenko]

Sorry if this is a dumb question, but is there a way for me to merge the changes in #9915 locally onto my computer for the time being?

Edit: I figured this out, and am now trying to write the proof again...

[Eric Wieser]

I hadn't noticed that @Aaron Liu got the PR building, I'll try to find time to review it

[Willem vanhulle]

Peter Hansen zei:

Maybe field_simp is worth a mention:

example (lmd : NNReal) (h : lmd ≤  (1 / 2 : ENNReal))  : (2⁻¹ : ENNReal) + 2⁻¹ + ↑lmd - ↑lmd = 2⁻¹ + ↑lmd + (2⁻¹ - ↑lmd) := by
  field_simp

field_simp is not that powerful for me. For example, it cannot prove:

lemma test_inv_div_mul_div {a b c : ℕ} :
  (1 / (↑a : ENNReal))⁻¹ * ((↑b : ENNReal) / (↑c : ENNReal)) = (↑(a * b) : ENNReal) / (↑c : ENNNReal)

[Kevin Buzzard]

field_simp works great for fields (like the reals) (the clue is in the name) but ENNReal is not a field (so your mileage may vary) (basically it's useful "sometimes").

[Willem vanhulle]

I am trying to build a tactic that can solve most common expressions in ENNReal, but maybe someone else has tried already? I am new to tactics, so I am struggling making the normalization of arithmetic ENNReal expressions unique to enable goal with assumption matching.

[Kevin Buzzard]

I went to a course on tactic-writing recently and whilst I still would not say that I can write tactics at all, one thing I learnt was the first step, which is to first write the tests, and then write the Lean proofs of the tests which you want the tactic to find; this might involve proving new lemmas along the way (manually, not using the tactic). Once you have this, you're in a position to start thinking about how to write the tactic.

[Willem vanhulle]

Kevin Buzzard zei:

I went to a course on tactic-writing recently and whilst I still would not say that I can write tactics at all, one thing I learnt was the first step, which is to first write the tests, and then write the Lean proofs of the tests which you want the tactic to find; this might involve proving new lemmas along the way (manually, not using the tactic). Once you have this, you're in a position to start thinking about how to write the tactic.

Where do you find this kind of courses? I also wrote a lot of tests, but is hard to write generic tactics that work with many types of expressions.

[Kevin Buzzard]

Oh it was an in-person thing at my university, we have quite a big Lean group there.

[Alex Kontorovich]

We recorded @Heather Macbeth's version of this course at the Simons workshop; it'll hopefully make its way to YouTube soon, so others can also learn from her!

[Willem vanhulle]

I implemented a tactic to simplify ENNReal expressions: https://github.com/wvhulle/ennreal-arith

It is probably incredibly messy (my first Lean package).

[Willem vanhulle]

I managed to use it successfully for my Monty Hall frequentist solution https://github.com/wvhulle/learn-lean-riddles/blob/main/RiddleProofs/MontyHall/Dilemma.lean

[Michael Rothgang]

Willem vanhulle said:

I implemented a tactic to simplify ENNReal expressions: https://github.com/wvhulle/ennreal-arith

It is probably incredibly messy (my first Lean package).

I am very excited to see further automation towards working with ENNReal; this is sorely needed. I wonder about the next step: what would it take to make this (or something similar) part of mathlib?

[Michael Rothgang]

I can think of the following being useful:

• overall approach: discuss the high-level strategy first. Your repository doesn't mention how the tactic works; it could be useful to start a discussion about this on zulip (to identify an approach that's robust enough)
• documentation: the tactic implementation is split across half a dozen files, so I'm having a hard time getting an overview. An overview of the separate tactics you're writing, what they do (and do not do) and how one is supposed to use them could help. (To explain your current approach for the previous step, this will also help.)
• implementation. I could imagine splitting implementation into one file (or perhaps several) and the tests elsewhere may help. (I don't have a strong opinion on this yet.)

[Michael Rothgang]

One quick observation: you seem to be using the field_simp tactic (so, building on simp --- I presume). That tactic is currently being rewritten by @Arend Mellendijk, @Heather Macbeth and myself (using a different strategy, more similar to the module tactic). I wonder if building a tactic on simp is the most robust approach.

[Willem vanhulle]

@Michael Rothgang, @Kevin Buzzard I have refactored the ennreal_arith tactic a lot. But now I am kind of stuck with a lot of if then else on the goal shape. Would it be best if I switch to quote4 / qq for pattern matching on expressions? I saw it was used in the definition of Mathlib's ring1, but it is a bit difficult for me to understand.

Here is an example of the code using if then instead of matching https://github.com/wvhulle/ennreal-arith/blob/main/ENNRealArith/ArithmeticCore.lean

[Eric Wieser]

Eric Wieser said:

I hadn't noticed that Aaron Liu got #9915 building, I'll try to find time to review it

I've brought this back up to speed with master, so it should build again.

[Willem vanhulle]

@Michael Rothgang Well, I have rewritten all of the tactic logic. Before, I relied too much on LLM output. Now I think I know better how all the tactcs work internally. https://github.com/wvhulle/ennreal-arith