Entropy on an infinite type

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

I just realized there is a non-trivial technical issue required to even formalize the weak PFR over Z stuff: all of our entropy machinery currently requires the random variables to take values in a finite set (or more precisely a Fintype), but of course the integers (or Z^d) are infinite. So we may have to generalize the entirety of our entropy and Ruzsa distance machinery to random variables that have finite image, as opposed to taking values in a Fintype. (This is also the natural extension from a mathematical point of view - one could even extend further to random variables with countable image, but finite image should suffice for many applications.)

Hopefully this won't be utterly painful. I guess we need to create instances [FiniteImage X] for our random variables and show that they are automaticallly instantiated when the range G is a Fintype, and are also automatically preserved by pointwise operations such as X+Y, X-Y, and ⟨ X, Y ⟩. For most of our entropy/Ruzsa distance stuff it should then just be OK to replace various [Fintype G] hypotheses with [FiniteImage X] hypotheses; it should only be the very foundational entropy inequality stuff where some actual work is required.

If there are any Lean experts who are familiar with this sort of refactoring experience, any advice would be appreciated. I'm guessing the first step should be to define the FiniteImage property (it doesn't already seem to be in Mathlib) and create some instances?

[Shreyas Srinivas]

the standard technique is to create a typeclass.

class FiniteImage (f : <Type Signature of f>) where
     property1 : <Property>
     property2 : <Property>
     ...

[Yaël Dillies]

Do we want finite image, or rather finite measure?

[Terence Tao]

OK, so something like

import Mathlib

class FiniteImage {Ω G : Type*} (X : Ω → G) where
  hfinite : Set.Finite (X '' Set.univ)

I guess? Then we would need instances that say for instance if G is a Fintype then X is automatically FiniteImage, if X has FiniteImage then so does f ∘ X for any function f, and so forth.

[Terence Tao]

Yaël Dillies said:

Do we want finite image, or rather finite measure?

Actually the most natural property would be finite entropy, i.e., that the sum $H[X] = \sum_{x \in G} {\bf P}[x \in G] \log \frac{1}{{\bf P}[x \in G]}$ is finite. But finite image would suffice for our application here.

[Terence Tao]

I'm not sure what the pros and cons of either approach are.

Actually, if we're going to use typeclasses, then I could package other things as well:

import Mathlib

open MeasureTheory ProbabilityTheory

class DiscreteRandomVariable {Ω G : Type*} (X : Ω → G) where
  hΩ: MeasurableSpace Ω
  hG: MeasurableSpace G
  hG_singleton: MeasurableSingletonClass G
  hmes : Measurable X
  hfinite : Set.Finite (X '' Set.univ)

(or maybe I should move hΩ, hG, hG_singleton into instances in the class definition?)

This would require a bit more refactoring but could potentially be a cleaner and more conceptual way to proceed in the long run.

[Sebastien Gouezel]

Just to clarify, when I claimed Improved PFR, I meant the missing content in the file ImprovedPFR.lean (corresponding roughly to B.2, B.3, B.4, B.5, B.6, B.7 and C.1, C.2, C.3). I started on the file, but of course I'm not nearly done yet, and I can definitely share it with whoever would like to work on it! The current state of things is in https://github.com/teorth/pfr/pull/141, in case other people want to start from there.

[Kyle Miller]

f '' Set.univ is also known as Set.range f by the way, so you could do

def FiniteRange {Ω G : Type*} (f : Ω → G) := (Set.range f).Finite

Regarding the design decision between a definition and a class:

• If you're going to rw terms or otherwise manipulate algebraic expressions, use a def (like how Set.Finite is a def)
• Otherwise, if you're going to avoid manipulating the terms, and also having it infer instances based on the syntactic structure of terms would be very convenient (like the X+Y, X-Y, etc you mentioned), you can use a class (like how Finite is a class)

[Kyle Miller]

The problem with classes is that instance search isn't stable under rewriting. You might start with a term for which there is an instance, but after a rewrite typeclass inference might no longer be able to find an instance. You have to weigh out whether the convenience of getting instances is enough to counteract this issue.

[Kyle Miller]

Don't forget to include : Prop to make sure the class is a proposition. Otherwise I think it defaults to Type.

class FiniteRange {Ω G : Type*} (X : Ω → G) : Prop where
  hfinite : (Set.range X).Finite

[Terence Tao]

Hmm. If we have an instance lemma that automatically gives FiniteRange X whenever Fintype G, then hopefully every single previous usage of entropy stuff in PFR won't break, and so it's only the new stuff in the PFR over the integers that needs some attention. I imagine we can always add more instance lemmas if the rewrite issue shows up, so I'm leaning towards the typeclass solution. (Being able to automatically handle measurability is another bonus, but not really necessary since we already developed the entire entropy library with measurability hypotheses manually added as side conditions as needed.)

[Kyle Miller]

I'll also mention that I bring up Set.Finite and Finite as examples because they illustrate that sometimes you want both. Part of the API of these is to be able to easily go back and forth between them, hence docs#Set.toFinite and docs#Set.Finite.to_subtype

That might not be too representative though since Finite is for types in general, and using Set.Finite saves needing to worry about that coercion to type.

[Terence Tao]

OK. I have to attend to other things for a few hours but later today I might get started on a basic FiniteRange API. I would also be interested in @Rémy Degenne's opinion on how difficult it would be to refactor the foundational entropy inequality stuff to handle FiniteRange random variables as opposed to Fintype ranges. I'm hoping that only the most basic tools need to be actually modified, and all the other lemmas that are built on top will automagically carry over through the power of polymorphism or something.

[Kyle Miller]

(If you need to create local Fintype instances during this refactor, then it's worth knowing that the pattern is, given h : Set.Finite s, you write have := h.fintype in your proof. You could create such a docs#Set.Finite.fintype function specialized for your typeclass too. I'm thinking you'd write have := FiniteRange.fintype X to get Fintype (Set.range X) from FiniteRange X?)

[Kyle Miller]

Feel free to name that field finite instead of hfinite, so then you could write have := FiniteRange.finite X to get Finite (Set.range X) by parallelism.

[Terence Tao]

So would you recommend something like this?

import Mathlib

class FiniteRange {Ω G : Type*} (X : Ω → G) : Prop where
  finite : (Set.range X).Finite

noncomputable def FiniteRange.fintype {Ω G : Type*} (X : Ω → G) [hX: FiniteRange X] : Fintype (Set.range X) := hX.finite.fintype

[Terence Tao]

(deleted)

[Notification Bot]

17 messages were moved here from #Polynomial Freiman-Ruzsa conjecture > Outstanding tasks, version 7.0 by Yaël Dillies.

[Yaël Dillies]

I do not quite grasp yet why finite range is the correct generality here. It seems to me like it would be much easier (and not involve any new class) to use @Rémy Degenne's entropy of a measure instead of the fintype entropy we've been using so far. See PFR.ForMathlib.Entropy.Measure.

[Yaël Dillies]

The entropy of a random variable would then be the measure entropy of its law.

[Yaël Dillies]

Rémy, does that sound reasonable?

[Sebastien Gouezel]

Rémy's definition currently only makes sense on a fintype, right?

[Yaël Dillies]

Oh you're right. We need Kullback-Leibler in general :sad:

[Yaël Dillies]

https://en.wikipedia.org/wiki/Kullback%E2%80%93Leibler_divergence#Definition seems pretty palatable. Sébastien, do you see any obvious obstruction to just doing it? That would let us have entropy in a good enough generality for mathlib (I'm currently not very happy with our generality).

[Terence Tao]

I suppose we could try to replace all Finset.sum appearances in the foundational entropy material with tsum and hope for the best (inserting hypotheses of finite entropy whenever necessary, and having an additional lemma that the entropy is finite whenever either the range is a Fintype or the random variable has finite range).

[Terence Tao]

Also we would need that the finite entropy hypothesis is preserved by pairing (if X, Y have finite entropy, then so does ⟨X, Y⟩) and by applying measurable functions (if X has finite entropy then so does f ∘ X) but these look doable.

[Terence Tao]

I think the finite range approach would be slightly quicker to implement if we only cared about PFR, but I see that the general approach (inserting finite entropy hypotheses as needed) would be better for Mathlib.

[Rémy Degenne]

Yaël Dillies said:

https://en.wikipedia.org/wiki/Kullback%E2%80%93Leibler_divergence#Definition seems pretty palatable. Sébastien, do you see any obvious obstruction to just doing it? That would let us have entropy in a good enough generality for mathlib (I'm currently not very happy with our generality).

Defining the Kullback-Leibler divergence is the goal I have been working towards with my recent mathlib PRs about rnDeriv, withDensity and tilted measures. There is more work on branch#RD_kl (warning: that branch is a mess that also contains unrelated things), where I prove that KL is nonnegative and prove a Donsker-Varadhan variational formula.

For PFR, extending to functions with finite ranges seems far simpler. And once the measure entropy definition is changed, most of the other definitions should require only minimal modifications.

[Rémy Degenne]

I am attending a conference this week and will do only minimal coding, so someone else should write the generalization.

[Terence Tao]

Perhaps a compromise is to extend the basic definitions of entropy to handle infinite ranges, but add for now a finite range hypothesis to most of the foundational methods, and as a future project seek to relax these hypotheses to a finite entropy hypothesis (and possibly some methods may even work in the infinite entropy case if the definitions are chosen correctly).

[Terence Tao]

So one could imagine the following refactoring process:

1. Keep the Fintype G type hypotheses in place, but replace Finset.sum with tsum in the core definitions and do whatever modifications are needed to make everything build.
2. Now remove Fintype hypotheses from the core definitions, but move them to all of the methods (or the ambient hypotheses in whatever section the methods appear in). This should not affect the build significantly.
3. For each method, gradually replace Fintype G with FiniteRange X type hypotheses. Ideally this would only require actual changes in code for the first few methods, and many of the downstream methods would not need any modification other than the hypothesis change. This would be enough to get started on the PFR over the integers extension. This part of the process could potentially be parallelized through the "Outstanding tasks" board.
4. At some much later date, see if FiniteRange X type hypotheses can be relaxed further to FiniteEntropy X type hypotheses.

Alternatively one could try to do 2 + 3 in one go which might be a little faster overall, but create a longer gap in which one no longer has a working build.

[Kevin Buzzard]

When mathlib redefined the concept of a group we always had a working build because the development was done on a feature branch and only merged to master once it was completely working.

[Terence Tao]

I guess I have a technical question then - if I already have administrator privileges on a repository, what is the best way in VsCode to create a branch of the repository to do a complex refactoring that would temporarily break the build?

[Yaël Dillies]

I would simply click on the branch name master in the lower left and create a branch from
this interface.

[Yaël Dillies]

Our CI didn't run on branches (this was semi-intentional). I now have activated CI for branches. Tell me if it works!

[Terence Tao]

OK, I created a branch. So on the local side I would create a completely new folder to hold the branch, and open that folder within VSCode?

[Yaël Dillies]

Nonono, you would kill one of the very points of Git :smile: You use the VSCode interface to "checkout" different branches, by clicking on the branch name in the lower left.

[llllvvuu]

It should be all the same files/folder paths; the branch bookkeeping is done by git (technically in the hidden folder .git)

[llllvvuu]

git checkout just swaps out the files

[Terence Tao]

OK. I think I checked out the "entropy_refactor" branch and made a small edit (breaking the build, haha). Let's see if this works.

[Terence Tao]

OK I think I only messed up the branch and not the master. Thanks, I think I can work with this.

[Yaël Dillies]

CI is working as expected!

[Terence Tao]

OK. I think I can steadily go through the broken build (in which I replaced Finset.sum with tsum in the definition of entropy of a measure) fixing each lemma as I go along, either by replacing a Finset.sum method with a tsum counterpart, or by adding a suitable Fintype or FiniteRange hypothesis. It's surprisingly smooth going so far (got 200 lines of measure.lean refactored already). Will be a while before the branch has a fully working build again, but that's not a problem as long as the master remains untouched.