Outstanding tasks, version 7.0

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

The second phase of the PFR project is well and truly underway! Previous outstanding tasks thread can be found here.

A. Existing claims

1. @Yaël Dillies is gradually porting various stable PFR files over to Mathlib. Expect frequent Mathlib bumps during this process. It should be possible to work on extensions concurrently with this porting.
2. @Paul Lezeau has formalized Additive energy and Cauchy-Schwarz bound, and has completed the proof of the latter.
3. @Yaël Dillies and @Bhavik Mehta claim the proof of Balog-Szemeredi-Gowers
4. @Sebastien Gouezel has established Improved PFR.

B. Outstanding proof formalization tasks:

1. Approximate homomorphism form of PFR. This is a variant of the already-proven Homomorphism form of PFR and should be relatively straightforward to prove by an adaptation of that proof. Claimed by @Eric Rodriguez
2. Constructing good variables, I' This should be a slight modification of Constructing good variables, I. Established by @Sebastien Gouezel
3. Constructing good variables, II' This should be a routine variant of Constructing good variables, II. Awaits C.1. Established by @Sebastien Gouezel
4. Constructing good variables, III' Should follow from preceding result and the arguments used to prove tau decrement. Awaits C.1, C.2. Establishedby @Sebastien Gouezel
5. General inequality Mostly taking linear combinations of other inequalities. There is one tricky new thing, which is to show that a certain conditioned random variable has identical distribution to the sum of two other conditioned random variables. Established by @Sebastien Gouezel
6. Bound on distance differences Mostly taking linear combinations of other inequalities. A slight refactoring of Second estimate will be needed. Awaits C.3. Established by @Sebastien Gouezel
7. Improved tau decrement A straightforward variant of (the second half of the proof of) tau decrement. Awaits C.2, C.3. Established by @Sebastien Gouezel
8. Entropy form of PFR' Straightforward modification of Entropy form of PFR.
9. Torsion-free doubling This is similar to many other entropy inequalities already in PFR, though somewhat lengthy. Awaits C.4.
10. Torsion distance shrinking Easy corollary of B.9. Awaits C.4, C.5.
11. Apply entropic PFR Easy application of existing PFR lemmas. Awaits C.6.
12. PFR projection One tricky thing is to locate a maximal subgroup H obeying a certain property, and show that the quotient is still an elementary abelian 2-group. Awaits C.6, C.7.
13. Single fibres Involves some manipulations of finite sums, but nothing too intimidating I think. Awaits C.8.
14. Asymmetric weak PFR Involves a strong induction, but should be doable. Awaits C.7, C.8, C.9, C.10.
15. Symmetric weak PFR Easy corollary of B.14. Awaits C.9, C.10, C.11.
16. Weak PFR over integers Easy corollary of B.15. Awaits C.11, C.12.
17. Refactor existing entropy / Ruzsa distance machinery to handle cases when G is not a Fintype, but instead X is assumed to be of FiniteRange. Established by @Terence Tao

C. Outstanding documentation/blueprint/examples/statement formalization tasks:

1. Constructing good variables, II' Here the sum involves 12 terms, one may need to think about the cleanest way to express this formula. Established by @Sebastien Gouezel
2. Constructing good variables, III' Similar issue to preceding. Established by @Sebastien Gouezel
3. Bound on distance differences Involves the sum of 12 terms appearing in C.3, but should otherwise be simple to state. Claimed by @Sebastien Gouezel
4. Torsion-free doubling This is similar to many other entropy inequalities already in PFR and should be easy to formalize. Claimed by @Paul Lezeau
5. Torsion distance shrinking Also should be easy to formalize. Claimed by @Paul Lezeau
6. Apply entropic PFR Also straightforward to formalize.
7. PFR projection Also straightforward.
8. Single fibres A bit messy, but straightforward.
9. Dimension Should be definable using linear algebra methods in Mathlib. Established by @Paul Lezeau
10. Asymmetric weak PFR Straightforward to formalize. Awaits C.9.
11. Symmetric weak PFR Also straightforward. Awaits C.9.
12. Weak PFR over integers Also straightforward. Awaits C.9.
13. Introduce a notion of FiniteRange and state some of its basic properties. Established by @Terence Tao

D. Outstanding administrative tasks:

1. Create a new Lean file for Weak PFR over Z and put in stubs for all the new definitions and lemmas. Established by @Terence Tao
2. Add example showcasing weak PFR to examples.lean. Awaits C.12.
3. Update HomPFR, ApproxHomPFR, PFR_conjecture', examples.lean to accommodate the improvement of constants from 12 to 11.

[Eric Rodriguez]

I'd be happy to try B.1!

[Paul Lezeau]

I'd like to claim C4 and C5!

[Terence Tao]

Paul Lezeau said:

I'd like to claim C4 and C5!

Great! There is one catch right now, which is our definition of entropy requires that the range G is a Fintype, which is not the case over the integers. I'm working right now to extend the definition of entropy (assuming instead that random variables have finite range) without breaking the build, but I have only achieved the first task so far (i.e., I have extended the definition, but at the cost of breaking the build; you can see the broken version at https://github.com/teorth/pfr/tree/entropy_refactor ). One may have to temporarily introduce a placeholder notion of entropy in order to formalize the lemmas, and switch them back to the actual notion of entropy when they are formalized. (I did formalize the notion of finite range though, see https://github.com/teorth/pfr/blob/master/PFR/ForMathlib/FiniteRange.lean ).

[Terence Tao]

Here is the precise definition I am using; the difference from the previous version is that a Finset.sum is now a tsum, and the Fintype S hypothesis has now been removed.

import PFR.ForMathlib.MeasureReal
import PFR.ForMathlib.FiniteRange
import PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog
import PFR.Mathlib.Data.Fintype.Card

open Real MeasureTheory
open scoped ENNReal NNReal Topology BigOperators

namespace ProbabilityTheory
variable {S : Type*} [MeasurableSpace S] [MeasurableSingletonClass S]

def measureEntropy (μ : Measure S := by volume_tac) : ℝ :=
  ∑' s, negMulLog (((μ Set.univ)⁻¹ • μ) {s}).toReal

[Paul Lezeau]

Okay noted! I'm quite happy to wait a bit until you're done

[Paul Lezeau]

In the meantime I can do C9 since that one doesn't depend on anything

[Terence Tao]

I'll use this message to update on the status of the entropy refactoring. The following files potentially need refactoring, in rough order of dependency:

1. PFR.ForMathlib.Entropy.Measure refactored
2. PFR.Mathlib.Probability.Kernel.Disintegration refactored
3. PFR.ForMathlib.Entropy.Kernel.Basic refactored
4. PFR.ForMathlib.Entropy.Kernel.MutualInfo refactored
5. PFR.ForMathlib.Uniform refactored
6. PFR.ForMathlib.Entropy.Basic refactored
7. PFR.ForMathlib.Entropy.Kernel.Group refactored
8. PFR.ForMathlib.Entropy.Group refactored
9. PFR.ForMathlib.Entropy.Kernel.RuzsaDist refactored
10. PFR.Mathlib.Probability.IdentDistrib refactored
11. PFR.ForMathlib.Entropy.RuzsaDist refactored
12. PFR.Fibring refactored
13. PFR.TauFunctional refactored
14. PFR.FirstEstimate refactored
15. PFR.SecondEstimate refactored
16. PFR.Endgame refactored
17. PFR.HundredPercent refactored
18. PFR.Main refactored
19. PFR.improvedPFR refactored
20. Merging back into master done

I will be going down the list one by one. The first one took me the better part of a day, but I am hoping that the later ones will be quicker as they rarely involve the low-level implementation of entropy directly.

Some other files that ended up being modified (mostly by adding variants of existing lemmas):

1. PFR.Mathlib.MeasureTheory.Integral.Bochner
2. PFR.Mathlib.MeasureTheory.Integral.Lebesgue
3. PFR.Mathlib.Algebra.GroupWithZero.Units.Lemmas
4. PFR.ForMathlib.FiniteRange
5. PFR.Mathlib.Probability.Independence.Basic
6. PFR.Mathlib.Probability.Independence.Kernel
7. PFR.Mathlib.Data.Fin.VecNotation

In refactoring Disintegration.lean I found it convenient to impose countability conditions on the various measure spaces, which is slightly unsatisfactory, but good enough for our applications since the integers are countable.

Some other changes: a few of the lemmas about isUniform now require that the set H that one is uniform over is a Finset rather than a Set, which causes some slightly annoying changes to existing code using this concept (a couple appearances of .toFinite.toFinset show up).

Many applications of integral_eq_sum should now use integral_eq_finset' instead. This latter method pairs well with FiniteRange.null_of_compl. For instance, I had to adjust integral_eq_sum to integral_eq_sum_finset' _ _ (FiniteRange.null_of_compl hT₃ _) in the preliminary version of PFR.improvedPFR.

Any new entropy lemmas that don't assume the random variables take values in a Fintype will most probably need to register FiniteRange instances for the random variables instead.

There is also some weird motive issue I don't understand that forced me to replace some rw with simp_rw.

[Terence Tao]

Terence Tao said:

10. PFR.ForMathlib.Entropy.RuzsaDist in progress

Ugh, I have hit a snag at the very end of the refactoring progress.

I managed to successfully refactor the first nine files to allow for random variables with finite range in a Countable type, as opposed to ranging in a Fintype. Along the way I developed an API for FiniteRange vraiables, as well as the related concept of a measure having FiniteSupport, and a probability kernel having FiniteKernelSupport. So far, so good. In particular, instances of FiniteRange propagate very nicely with respect to operations such as adding or subtracting two random variables.

However, there is a technical issue: when taking independent copies of two random variables X: Ω → G, Y: Ω' → G of finite range, the current construction gives variables X' : Ω' → G, Y' : Ω' → G that technically can be of infinite range. Indeed we are taking the sample space Ω' to be G × G, with X' ω = ω.1 and Y' ω = ω.2, and these random variables have infinite range when G is infinite.

One way out is to try to develop a notion of EssentialFiniteRange for a random variable, so that it is finitely valued outside of a null set. But then the notion depends on the measure μ as well as the function X. But then it is hard to automatically grant instances to such an object unless one packages it into a single RandomVariable class - but then there are a lot of coercions between RandomVariables and the underlying function which become unpleasant.

The other way out is to create alternate versions of the independence construction part of the project in which that one trims the sample space down to the product of ranges. This is not too bad for products of two spaces, but to take products of multiple spaces one starts to enter the infamous "dependent type hell". And unfortunately we will need to take products of three or four spaces here. (A possible inelegant compromise here would be to still work with the product of the original G spaces, modify the projection operators x ↦ x.1, x ↦ x.2 outside of the ranges of the random variables to send them to some dummy value, such as G.choose, purely in order to recover the FiniteRange property.)

I am thinking of working with an alternate approach to jointly independent copies that which one gets a triple or quadruple of independent copies by iterating the pair construction a few times, and introducing an additional independence lemma to deduce joint independence of say X, Y, Z from pairwise independence of X and Y, as well as pairwise independence of ⟨ X, Y ⟩ and Z. It's doable, but it may take some effort.

Will have to think about how best to proceed here. Any suggestions would of course be welcome.

[Terence Tao]

OK, I think I see a path forward. We keep the existing independent copy constructions, but add corollaries that if all the input variables are FiniteRange then one can modify the independent copies on a null probability event to also be of FiniteRange. There are existing Mathlib methods that show that such modifications preserve joint independence. One then has to replace the appeal to independent copy constructions to ones that also guarantee FiniteRange.

[Yaël Dillies]

That second approach sounds reasonable, yes.

[Terence Tao]

It took longer than expected, but I finally managed to refactor all the entropy files (and the PFR files that depend on entropy) so that they no longer require the codomain of the random variables to be finite, but instead that the random variables have FiniteRange. (So instances of the form [FiniteRange X] will be needed throughout the weak PFR file, since they can't be gained automatically from the finiteness of the codomain.)

I've merged things back into the master branch, and now formalization can begin on weak PFR. There are some residual build issues coming from trying to align @Sebastien Gouezel 's partial progress on improved_PFR into the new framework, but I'm almost done with cleaning that up. (Sebastien, I hope this doesn't cause too many merge conflict headaches on your end...)

[Sebastien Gouezel]

I've finally finished the exponent improvement to the main result, getting from 2K^{12} to 2K^{11}. Some parts were quite painful (when arguing by symmetry over 6 permutations, I had to do a lot more by hand than would be reasonable). But the final part of the argument went like a breeze (just copy-pasting the argument for 2K^{12}, and replacing a constant here or there when Lean was complaining).

[Sebastien Gouezel]

Would it make sense to improve the constants in the file HomPFR, just for the sake of definiteness?

[Sebastien Gouezel]

Also, I've linted the project, and the simpNF linter complains that we use Nat.card s instead of Set.ncard s. I wasn't aware that we had these two equivalent definitions in the library (the difference is that in Nat.card s then s is first coerced to a type, but one always has Nat.card s = Set.ncard s). Is it an oversight that we have both in the library, or is there a good reason to keep both?

[Terence Tao]

Sebastien Gouezel said:

Would it make sense to improve the constants in the file HomPFR, just for the sake of definiteness?

Sure, it should be easy now to improve the constants in HomPFR and also PFR_conjecture' and ApproxHomPFR (and update examples.lean accordingly).

[Terence Tao]

Sebastien Gouezel said:

Also, I've linted the project, and the simpNF linter complains that we use Nat.card s instead of Set.ncard s. I wasn't aware that we had these two equivalent definitions in the library (the difference is that in Nat.card s then s is first coerced to a type, but one always has Nat.card s = Set.ncard s). Is it an oversight that we have both in the library, or is there a good reason to keep both?

Huh. I guess there's no inherent reason we have to use Nat.card (actually I was toying with the idea of trying to use Finset.card instead, but then A needs to be made a Finset and suddenly Lean wants DecidableEq G in order to make sumsets work, and I mostly abandoned the idea, although some of the IsUniform code still works with Finsets which is perhaps a bit inefficient as it causes some annoying coercion workarounds, and one should probably work instead with Finite Sets, but the code was compiling so I didn't try to fix it). I don't see any downside to replacing Nat.card with Set.ncard throughout (and then we get to also use dot notation), but maybe some people more familiar with Mathlib will have a more informed opinion.

[Terence Tao]

Sebastien Gouezel said:

I've finally finished the exponent improvement to the main result, getting from 2K^{12} to 2K^{11}. Some parts were quite painful (when arguing by symmetry over 6 permutations, I had to do a lot more by hand than would be reasonable). But the final part of the argument went like a breeze (just copy-pasting the argument for 2K^{12}, and replacing a constant here or there when Lean was complaining).

Thanks so much for pushing through that entire argument! In particular I'm glad that the entropy refactor didn't disrupt the process. And this is the one place in the project where there could conceivably have been numerical errors in the argument (and indeed the original blueprint version contained some nontrivial typos) - this argument didn't undergo the same round of repeated review by myself and my three coauthors - so the formal verification really counts for something here.

[Yaël Dillies]

@Peter Nelson was the one defining docs#Set.ncard and I'm not entirely sure why we have it.

[Yaël Dillies]

I would understand we could have it for set notation if it were to be an abbreviation for Nat.card ↥s, but instead it goes through docs#PartENat !

[Yaël Dillies]

I don't think we should use it in PFR, at least not before it's actually seen some use in mathlib.

[Yaël Dillies]

For context, I was aware of the situation and decided to stick with Nat.card.

[Terence Tao]

Yaël Dillies said:

For context, I was aware of the situation and decided to stick with Nat.card.

I guess we should be consistent with what the additive combinatorics portion of Mathlib uses.

[Yaël Dillies]

Then we should use Finset.card!

[Yaël Dillies]

But Bhavik and I agree that this is not optimal once you start talking about subgroups. There's some figuring out to be done.

[Terence Tao]

Oh good point. Easier to work with a Finite AddSubgroup G than create a new FinAddSubgroup G class.

[Terence Tao]

Maybe some lemmas in the additive combinatorics library should have two versions, one for Finsets and one for Finite Sets.

[Peter Nelson]

It was @Jireh Loreaux who suggested changing the definition of ncard to be in terms of encard (and therefore indirectly via PartENat.card) rather than Nat.card. This was so that deriving the ncard API from the encard API went the smoothest.

[Peter Nelson]

Terence Tao said:

Maybe some lemmas in the additive combinatorics library should have two versions, one for Finsets and one for Finite Sets.

Yes - the Set API is so much nicer than Finset for many reasons.

[Yaël Dillies]

I strongly disagree with that!

[Peter Nelson]

Finset has horrible notation for intersections (with sets) and interaction with subtypes, forces Decidable fluff in lemma statements, and nothing is definitional.

[Terence Tao]

The main advantage of Finset I encountered in the PFR project is that one gets to use sum instead of tsum.

[Yaël Dillies]

Notation we're working on it. Definitionality I have a PR in the works. DecidableEq, point given, but it's actually pretty easy to get it right.

[Jireh Loreaux]

note: I think @Yury G. Kudryashov was going to refactor to remove PartENat in favor of just ENat, but I'm not sure if there is a PR yet.

[Terence Tao]

During the entropy refactor this issue annoyed me a fair bit until I learned about .toFinite.toFinset which mostly solved my coercion issues.

[Yury G. Kudryashov]

I get distracted every time.

[Yury G. Kudryashov]

Too many refactors I want to do.

[Peter Nelson]

Yes Finite.toFinset does help. But then you get underscores in the infoview (or you can turn them off, and suddenly referring to a set cardinality takes 20 characters). And simple things then become a cascade of simp only.

[Peter Nelson]

For me, the defeq in the way that Set is defined is intuitively priceless.

Part of my problem with Finset.card is how awkward it is to make statements like 'there are at most 100 Fermat primes'.

[Terence Tao]

I guess Finsets are intended only for sets that are "definitionally" finite, as opposed to ones that are only "accidentally" finite.

[Peter Nelson]

Terence Tao said:

I guess Finsets are intended only for sets that are "definitionally" finite, as opposed to ones that are only "accidentally" finite.

Yes, or 'maybe finite'.

[Terence Tao]

It all seems to me to be an artefact of Lean's preference for avoiding dependent types. Otherwise we could replace Finsets with Finite Sets everywhere.

[Terence Tao]

Actually, while on this topic: why do we have both Finite and Set.Finite?

[Eric Rodriguez]

Terence Tao said:

It all seems to me to be an artefact of Lean's preference for avoiding dependent types. Otherwise we could replace Finsets with Finite Sets everywhere.

For maths, I think that'd be a decent state of affairs, but it means we'd lose computability of (some) finite sets, which can be useful in many circumstances (usually, exactly the same ones where we'd want to evaluate a "sufficiently small" set in paper maths). In programming, Sets are almost useless, as far as I understand

[Terence Tao]

Ah, right, finiteness is definitely more subtle in constructivist settings than classical ones.

[Yury G. Kudryashov]

Terence Tao said:

Actually, while on this topic: why do we have both Finite and Set.Finite?

We had docs#Set.Finite before we've got docs#Finite. We should redefine Set.Finite s as _root_.Finite s some day.

[Yury G. Kudryashov]

I don't know whether we should completely drop Set.Finite because _root_.Finite (s ∪ t) tries to interpret ∪ as an operation on types.

[Yury G. Kudryashov]

Or we can leave it as an abbrev.

[Yaël Dillies]

One of the reasons this wasn't done before is because it would have made docs3#set.finite a class, and that would have prevented rewriting set.finite hypotheses in the infoview because of the frozen instance cache (it's not a thing in Lean 4). We had the same problem with docs3#is_closed.

[Terence Tao]

abbrev sounds like a good compromise. Certainly the current situation is unwieldy. I had to write a conversion matrix between the six different types of finiteness - a finite Set, a Finset, a finiteType, a Fintype instance, a Set.Finite instance, and a Finite instance - to understand what was going on (see the "Finite sets" tab at https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo/edit#gid=0).

[Yaël Dillies]

I only count five. Type is not finiteness by itself. You have either {α : Type*}, [Fintype α] or {α : Type*} [Finite α]. So you can get rid of one row and one column.

[Yaël Dillies]

Actually, Set and Set.finite also belong together. So that's rather four.

[Terence Tao]

Technically they are referred to by different names though: a finite set A is not the same thing as an instance hA : Set.Finite A of the finiteness of A, and similarly for { x // x ∈ A } and hf: Finite { x // x ∈ A }.

[Yury G. Kudryashov]

nit: you may have {α : Sort*} [Finite α], not only {α : Type*} [Finite α]

[Yury G. Kudryashov]

Ah, you mean Finite α, Fintie (s : Set α), and Set.Finite s.

[Yury G. Kudryashov]

IMHO, we should hide Fintype from math users.

[Yaël Dillies]

Terence Tao said:

Technically they are referred to by different names though: a finite set A is not the same thing as an instance hA : Set.finite A of the finiteness of A, and similarly for { x // x ∈ A } and hf: Finite { x // x ∈ A }.

Yes, but you cannot "convert" from (s : Set α) to (s : Set α) (hs : s.Finite), nor can you convert from {α : Type*} to {α : Type*} [Fintype α] or {α : Type*} [Finite α].

[Yaël Dillies]

Yury G. Kudryashov said:

IMHO, we should hide Fintype from math users.

That's... very controversial. Fintype brings in many niceties for mathematicians.

[Yury G. Kudryashov]

@Yaël Dillies Here are six reasonable finiteness assumptions: [Finite α], [Fintype α], Finite s, Fintype s, Set.Finite s, s : Finset α.

[Terence Tao]

Yaël Dillies said:

Terence Tao said:

Technically they are referred to by different names though: a finite set A is not the same thing as an instance hA : Set.finite A of the finiteness of A, and similarly for { x // x ∈ A } and hf: Finite { x // x ∈ A }.

Yes, but you cannot "convert" from (s : Set α) to (s : Set α) (hs : s.Finite), nor can you convert from {α : Type*} to {α : Type*} [Fintype α] or {α : Type*} [Finite α].

Ah, good point. I can concatenate two rows and two columns of my table.

[Yaël Dillies]

Yury G. Kudryashov said:

Yaël Dillies Here are six reasonable finiteness assumptions: [Finite α], [Fintype α], Finite s, Fintype s, Set.Finite s, s : Finset α.

Fintype s we do use (but it's really fringe), Finite s I've only ever seen when you want to restrict to a finite subspace.

[Peter Nelson]

Four is still a lot!

[Jireh Loreaux]

Yeah, but computability is sometimes very convenient.

[Peter Nelson]

I’ve only ever been exposed to the cost, rather than the convenience. And I’m a combinatorialist.

[Peter Nelson]

Perhaps that’s not 100% true - there are a few times I’ve been annoyed at formalizing some small case analysis that could probably have been decidably knocked off.

[Jireh Loreaux]

That's exactly the kind of thing I'm talking about. When there are more than just a few cases, it's very handy.

[Peter Nelson]

I care much more about sets that may or may not be finite, and making statements about the cardinality when they are finite.

[Eric Rodriguez]

No need to choose, that's the plus :)

[Terence Tao]

It was this final piece of the original PFR project supplied by @Johan Commelin that sold me on the usefulness of being able to work with small decidable types.