Outstanding tasks, version 8.0

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

Time for another rollover! The previous outstanding tasks thread can be found here.

Now that entropy and Ruzsa distance is refactored to handle FiniteRange random variables rather than random variables taking values in a Fintype, we can begin to make more substantial progress on Chapter 11 of the blueprint (Weak PFR over the integers). In particular there are two preliminary lemmas (B.1 and B.2) that I had neglected to notice in the new blueprint whose statements are now formalized, and should be particularly easy to fill in, I think. For most of the remaining lemmas in the section (B.3-B.9), we need to first formalize the statements before proving them (tasks C.1-C.6, together with the two formalization tasks already claimed by @Paul Lezeau ).

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. @Yaël Dillies and @Bhavik Mehta claim the proof of Balog-Szemeredi-Gowers
3. @Eric Rodriguez claims Approximate homomorphism form of PFR.
4. @Paul Lezeau claims the formalization of Torsion-free doubling and Torsion distance shrinking.
5. @Paul Lezeau claims the API for dimension.

B. Outstanding proof formalization tasks:

1. Distance from zero This should be an easy application of existing Ruzsa distance inequality machinery. Established by @Jonas Bayer
2. Fibring inequality This should be an easy corollary of General fibring identity and existing entropy machinery. Established by @Jonas Bayer
3. Projection entropy and distance An easy application of existing entropy inequalities.
4. Torsion-free doubling This is similar to many other entropy inequalities already in PFR, though somewhat lengthy. Awaits formalization.
5. Torsion distance shrinking Easy corollary of B.4. Awaits formalization.
6. Apply entropic PFR Easy application of existing PFR lemmas.
7. 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.
8. Single fibres Involves some manipulations of finite sums, but nothing too intimidating I think.
9. Asymmetric weak PFR Involves a strong induction, but should be doable.
10. Symmetric weak PFR Easy corollary of B.9.
11. Weak PFR over integers Easy corollary of B.9.

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

1. Apply entropic PFR Should be straightforward to formalize. Completed by @Terence Tao
2. PFR projection Also straightforward. Completed by @Terence Tao
3. Single fibres A bit messy, but straightforward. Completed by @Terence Tao
4. Asymmetric weak PFR Straightforward to formalize. Completed by @Terence Tao
5. Symmetric weak PFR Also straightforward. Completed by @Terence Tao
6. Weak PFR over integers Also straightforward. Completed by @Terence Tao

D. Outstanding administrative tasks:

1. Add example showcasing weak PFR to examples.lean. Completed by @Terence Tao
2. Update HomPFR, ApproxHomPFR, examples.lean to accommodate the improvement of constants from 12 to 11. Completed by @Terence Tao

[Paul Lezeau]

By the way, just to avoid duplication of work, I should mention I'm also currently working on some API for dimension (and filling out the sorries)

[Jonas Bayer]

I'd like to claim 1. Distance from zero unless anyone else has started working on that.

[Jonas Bayer]

The claim is formalized with the additional assumption IsProbabilityMeasure μ'. Do we need the version with IsFiniteMeasure? This would require some API changes: entropy_const in a IsFiniteMeasure version and also a new Mathlib lemma that connects Measure.prod and multiplication of a measure by a constant.

[Jonas Bayer]

The proof is in https://github.com/TBUGTB/pfr, but before PRing I'd like to clean up some of the git history in my fork.

[Terence Tao]

(deleted)

[Terence Tao]

Jonas Bayer said:

The claim is formalized with the additional assumption IsProbabilityMeasure μ'. Do we need the version with IsFiniteMeasure? This would require some API changes: entropy_const in a IsFiniteMeasure version and also a new Mathlib lemma that connects Measure.prod and multiplication of a measure by a constant.

IsProbabilityMeasure should suffice for all PFR applications I think. If it can be cheaply extended to IsFiniteMeasure, that's great, but it's a somewhat low priority.

[Jonas Bayer]

It seems to me that the proof of B.3 (Projection entropy and distance) is a bit strange. For example, it wants to add up inequalities but there is only one.

My idea would be to move the lemma to the fibring file and use the Fibring inequality. Then it's just applying ent_of_indep_diff_lower and using that $U$ is uniform on $H$.

I.e. I'd like to claim B.3 and could also update the proof in the blueprint if that is helpful.

[Thomas Bloom]

Yes, you're right - when I wrote the proof I was using the second equality as an inequality (i.e. X=Y implies X\leq Y), that's what I implicitly meant.

I like your proof, and it's certainly easier given the Fibring inequality has already been proved. Please do update the proof in the blueprint!

(There are probably other places, such as this, where I wrote down the most direct proof from first principles, following the Green-Manners-Tao paper, but given the other lemmas already proved for PFR there may well be shortcuts one can take.)

[Paul Lezeau]

Could I claim B.5?

[Terence Tao]

Just a heads up that I have started formalizing the tail end (B.9-B.11) of the weak PFR stuff; B.10 and B.11 were straightforward but B.9 is proving more challenging than anticipated (it took several hours, for instance, to show that if G is a free ℤ-module of rank n then the quotient group G/2G is an elementary abelian 2-group of cardinality 2^n), but I think I will be able to complete it.

In the course of doing so I found a number of minor typos in the specifications of the earlier lemmas in the preprint and had to make a few small changes (adding a countability hypothesis, changing strict inequality to equality, making some variables explicit instead of implicit, that sort of thing). This may have a small impact on @Jonas Bayer's formalization of B.3 and @Paul Lezeau's formalization of B.5.

[Terence Tao]

OK, B.9 is done, although it took a lot more adventures through the world of modules over the integers (and how to pass back and forth between them and abelian groups) than I expected.

In doing so I had to interact a little bit with @Paul Lezeau's dimension and dimension' API. I suspect that the current definition of dimension (the rank of the real span of A) is not equal to dimension' (which corresponds to affine rank rather than linear rank); for instance {1} in the integers has a dimension of 1 and a dimension' of zero. The relation between dimension and dimension' is not dimension A = dimension' A, but rather (I think) dimension (Set.prod {1} A) = dimension A (where Set.prod {1} A lives in ℤ × G).

It may be easier avoid tensoring with the reals entirely, and just define dimension A to be the rank (as an abelian group, or as a Z-module) of the (group or module) closure of A. I had some initial struggles with the API for modules in Mathlib but actually it's pretty comprehensive once I figured my way around, and one doesn't really need to have an ambient field to prove things.

[Yaël Dillies]

I must say I was surprised when tensoring with the reals was first mentioned. I too would expect it to be unnecessary.

[Paul Lezeau]

Ah great, I'm happy I don't have to prove the equality! The reason I did the formalization with the tensor product was to try and stay close to the blueprint (which first defines the dimension of A as the dimension of its span over the reals), but I was a bit confused because I couldn't find a proof that the two definitions were equivalent.

[Paul Lezeau]

I think the blueprint might have a typo there since it seems to claim that the two quantities I defined are equal - or am I just confusing myself?

[Terence Tao]

Your version has A instead of A-A. But having dimension A := FiniteDimensional.finrank ℤ (A-A) for instance should be fine.

[Terence Tao]

Yeah I guess the blueprint alternate version involving the reals is more of a remark to assist human intuition as to why it is called "dimension" than an essential component of the formalization.

[Paul Lezeau]

Terence Tao said:

Your version has A instead of A-A. But having dimension A := FiniteDimensional.finrank ℤ (A-A) for instance should be fine.

Oh I see, I was reading the - as a hyphen and not as a mathematical symbol!

[Terence Tao]

I was able to formalize the proof after the definition of dimension using just the definition of dimension', together with the already proven dimension'_le_of_coset_cover as well as the still unproven dimension_le_rank (technically I also use dimension_eq_dimension', but we could just delete dimension and work only with dimension' and it would be fine, as long as we prove dimension'_le_rank which should be straightforward.

[Paul Lezeau]

Paul Lezeau said:

Terence Tao said:

Your version has A instead of A-A. But having dimension A := FiniteDimensional.finrank ℤ (A-A) for instance should be fine.

Oh I see, I was reading the - as a hyphen and not as a mathematical symbol!

Yet another situation where the formalization is useful I guess :grinning_face_with_smiling_eyes:

[Paul Lezeau]

Terence Tao said:

I was able to formalize the proof after the definition of dimension using just the definition of dimension', together with the already proven dimension'_le_of_coset_cover as well as the still unproven dimension_le_rank (technically I also use dimension_eq_dimension', but we could just delete dimension and work only with dimension' and it would be fine, as long as we prove dimension'_le_rank which should be straightforward.

Okay nice! I'm happy to write a proof of dimension_le_rank tomorrow!

[Terence Tao]

It's still true I think that dimension' A = FiniteDimensional.finrank ℤ (A-A) (assuming that the ambient module is finite, and possibly also freeness is needed), and it would have shortened some of the proofs I already formalized, but it's no longer necessary to prove it.

[llllvvuu]

I started WIP on torsion-free doubling: https://github.com/teorth/pfr/pull/162

[llllvvuu]

torsion-free doubling (B.4) is done: https://github.com/teorth/pfr/pull/162

[llllvvuu]

I started WIP on single_fibres (B.8): https://github.com/teorth/pfr/pull/167

[Paul Lezeau]

Could I claim 6 (Apply entropic PFR) ?

[Mauricio Collares]

Can I claim the remaining item, B.7? If it turns out to be too tricky I'll put it back in the pile in a week.

[Jonas Bayer]

Unfortunately, I've not been able to make much progress with 3 partly because I was sick during the last weeks and partly because the proof I wanted to do (see above) got quite complicated on the instance side. So I'd like to put the task back for now, if someone else wants to work on it.

[Yaël Dillies]

Do you want to contribute any partial progress?

[Jonas Bayer]

My local file is currently in a somewhat chaotic state since moving the lemma to a different file was not as trivial as I thought. There are now both missing and potentially unnecessary instance assumptions and I don't have a good overview anymore. I'm not sure what I could share from that, it would probably be most efficient to start afresh...

[Terence Tao]

Jonas Bayer said:

Unfortunately, I've not been able to make much progress with 3 partly because I was sick during the last weeks and partly because the proof I wanted to do (see above) got quite complicated on the instance side. So I'd like to put the task back for now, if someone else wants to work on it.

No problem. If you have any words of wisdom about what to avoid for the next person to try this task, perhaps that would be helpful...

[llllvvuu]

Minor question @Jonas Bayer , does ent_of_indep_diff_lower (3.5) exist (I can't find it)? Or were you using max_entropy_sub_mutualInfo_le_entropy_add (3.3) directly

[llllvvuu]

single_fibres (B.8) is done: https://github.com/teorth/pfr/pull/167

[Paul Lezeau]

app_ent_PFR (B.6) is done: https://github.com/teorth/pfr/pull/174

[Paul Lezeau]

To be able to apply certain lemmas, I had to make some small modifications to the assumptions (e.g. replace MeasurableSpace Ω by MeasureSpace Ω) - is that fine?

[Yaël Dillies]

You should not use MeasureSpace Ω but instead feed in μ : Measure Ω to the lemmas you were trying to apply.

[Yaël Dillies]

You should not use MeasureSpace Ω but instead feed in μ : Measure Ω to the lemmas you were trying to apply.

[Yaël Dillies]

Mathematically, it's the same, but formally it's better.

[Paul Lezeau]

Yeah that's what I thought!

[Terence Tao]

In principle volume_tac gives the best of both worlds, in that you can feed in an explicit measure if you want, or just rely on the bundled MeasureSpace measure if you wanted to.

[Paul Lezeau]

In my case however I had to construct a p : refPackage Ω Ω' G and for those one needs MeasureSpace Ω right? A few of the lemmas I used also assumed MeasureSpace Ω (Edit: the only such lemma I could find in the proof is entropic_PFR_conjecture_improv', so it's possible the others aren't used in my proof anymore/were refactored to use MeasurableSpace)

[Yaël Dillies]

pfr#refPackage

[Yaël Dillies]

Hmm yeah that's a problem. We should fix refPackage.

[Terence Tao]

Well if it works for now, fixing it is lower priority than completing the remaining tasks.

[Yaël Dillies]

Sure, but it's just a matter of replacing [MeasureSpace Ω₀₂] by [MeasurableSpace Ω₀₂] (μ : Measure Ω₀₂). Not a huge change.

[Paul Lezeau]

By the way, in the proof of improved entropy PFR, shouldn't the statement $\tau [X_1; X_2] \le \tau[X_1^0, X_2^0]$ actually be $\tau [X_1; X_2] \le \tau[X_2^0, X_1^0]$ ? (this is what happens in the Lean proof)

[Sébastien Gouëzel]

refPackage should definitely keep a MeasureSpaceinstance, because that's the way we want to do probability: with an implicit measure. If you want to construct a refPackage, then you should indeed construct a MeasureSpace.

[Sébastien Gouëzel]

(deleted)

[Sébastien Gouëzel]

(deleted)

[Terence Tao]

By the way, is there some basic constructor such as

import Mathlib
open MeasureTheory

def MeasureSpace.mk {Ω:Type} [MeasurableSpace Ω] (μ: Measure Ω) : MeasureSpace Ω := { volume := μ }

to build a MeasureSpace from a MeasurableSpace and a Measure? With such a constructor (as well as volume_tac for the opposite direction) it's a triviality to pass back and forth between MeasureSpaces and MeasurableSpaces anyway.

[Terence Tao]

Paul Lezeau said:

By the way, in the proof of improved entropy PFR, shouldn't the statement $\tau [X_1; X_2] \le \tau[X_1^0, X_2^0]$ actually be $\tau [X_1; X_2] \le \tau[X_2^0, X_1^0]$ ? (this is what happens in the Lean proof)

Yeah, I think you're right, I'll update the blueprint accordingly. (Lots of little typos that the formalization is picking up!)

[Paul Lezeau]

Terence Tao said:

Paul Lezeau said:

By the way, in the proof of improved entropy PFR, shouldn't the statement $\tau [X_1; X_2] \le \tau[X_1^0, X_2^0]$ actually be $\tau [X_1; X_2] \le \tau[X_2^0, X_1^0]$ ? (this is what happens in the Lean proof)

Yeah, I think you're right, I'll update the blueprint accordingly. (Lots of little typos that the formalization is picking up!)

I think there's the same typo for the (unimproved) entropy PFR by the way

[Rémy Degenne]

Terence Tao said:

By the way, is there some basic constructor such as

import Mathlib
open MeasureTheory

def MeasureSpace.mk {Ω:Type} [MeasurableSpace Ω] (μ: Measure Ω) : MeasureSpace Ω := { volume := μ }

to build a MeasureSpace from a MeasurableSpace and a Measure? With such a constructor (as well as volume_tac for the opposite direction) it's a triviality to pass back and forth between MeasureSpaces and MeasurableSpaces anyway.

Yes, there is such a constructor, and it is called exactly that: MeasureSpace.mk μ will make a measure space with volume μ.

[Mauricio Collares]

@Paul Lezeau I noticed you changed hent: H[X;μ] + H[Y;μ'] > 44 * d[X;μ # Y;μ'] to hent: H[X] + H[Y] > 44 * d[X # Y] in the statement of app_ent_PFR. Was that intentional? If so, should I propagate the change to PFR_projection?

Edit: [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] also changed to [IsProbabilityMeasure (ℙ : Measure Ω)] [IsProbabilityMeasure (ℙ : Measure Ω')], and I guess the two changes are related.

[Paul Lezeau]

@Mauricio Collares ah so that was because I needed to assume MeasureSpace Ω instead of MeasurableSpace Ω to make some of the lemmas I was using applicable, and also work with the canonical measure coming from MeasureSpace Ω. However since we have a constructor to get a MeasureSpace so I might be able to return to the original formulation if that's better

[Mauricio Collares]

I think the only application of PFR_projection uses the canonical measure, so propagating the changes wouldn't be a big problem; I just wanted it to be a conscious decision. Let's wait for Tao's feedback.

[Mauricio Collares]

I also have a mathematical question regarding PFR_projection, which I'm posting in the hope that I'll slap my forehead as soon as I hit submit. In Lemma 11.4 of the blueprint, I don't understand the second-to-last displayed equation. Here is the corresponding place in my Lean code; all other remaining sorries should be trivial.

Being more concrete, the equation in question is

$$\mathbb{H}(\psi''(X))+\mathbb{H}(\psi''(Y))< \frac{\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))}{2}\leq 2^{1-\lvert H'\rvert}(\mathbb{H}(X)+\mathbb{H}(Y)).$$

Although $H'$ is defined, the $|H'|$ in the exponent seems like a typo. Assuming it is meant to be $H''$ (which would allow us to deduce $\mathbb{H}(\psi''(X))+\mathbb{H}(\psi''(Y))\leq 44d[\psi''(X);\psi''(Y)]$ by maximality), then I don't see why the last inequality follows. By hypothesis on $H$, it is true that

$$\frac{\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))}{2}\leq 2^{-\lvert H\rvert}(\mathbb{H}(X)+\mathbb{H}(Y)),$$

but we only have $|H| < |H''|$ and getting to

$$\frac{\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))}{2}\leq 2^{1-\lvert H''\rvert}(\mathbb{H}(X)+\mathbb{H}(Y))$$

from that would require the other direction. If the $H'$ was meant to be a $H$ instead, then I don't see how to use the maximality of $H$. I guess my confusion is that if $H''$ is "much larger" than $H$, then

$$\mathbb{H}(\psi''(X))+\mathbb{H}(\psi''(Y))< \frac{\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))}{2}$$

seems very "wasteful" at first glance, and we need to "get back to $H''$" somehow. I tried looking at the proof of Lemma 9.1 in https://arxiv.org/pdf/2306.13403.pdf but it uses a slightly different approach, which would mean redoing the Lean proof from scratch.

[Thomas Bloom]

Hmm yes, you're right, this is my fault (I adapted the proof from the paper to be more amenable to formalisation, but took an invalid shortcut.)

There's a relatively short change I think that will make it work, so you shouldn't have to redo from scratch. I'll post it in a few hours when I'm back at my laptop. Sorry about that!

[Mauricio Collares]

No worries (and no hurry)! Redoing it from scratch wouldn't be bad, but a short change is even better :)

[Terence Tao]

Mauricio Collares said:

I think the only application of PFR_projection uses the canonical measure, so propagating the changes wouldn't be a big problem; I just wanted it to be a conscious decision. Let's wait for Tao's feedback.

I have no strong preference either way, since it doesn't really affect the arguments either way and is mostly an aesthetic issue. I guess making the tools accept MeasurableSpace+Measure instead of MeasureSpace is very slightly more convenient to the end user (it saves them typing MeasureSpace.mk) but it is a very minor thing I think.

[Terence Tao]

Rémy Degenne said:

Yes, there is such a constructor, and it is called exactly that: MeasureSpace.mk μ will make a measure space with volume μ.

Where is this documented, by the way? I can see it exists via #check, but docs#MeasureTheory.MeasureSpace.mk just redirects to the definition of MeasureSpace, and I can't even locate this method in the source code. Is there some very general mk method that works for general classes?

[Riccardo Brasca]

A class is under the wood just a structure, that is an inductive type with only one constructor, called mk by default (this can be changed using the syntax ::). You have a look at #tpil, in this section.

[Riccardo Brasca]

If you write whatsnew in before the definition of the class you should see all the stuff automatically generated by Lean.

[llllvvuu]

I poked at B.3 (ent_of_proj_le) a bit: https://github.com/teorth/pfr/pull/175/files

Currently, H[X - U_H] = H[pi(X), U_H] seeems to be the tedious part because X - U_H and pi(X), U_H marginalize over X, U_H slightly differently so we can't just plug in entropy_eq_of_injective or similar. I think we have to actually manipulate the sum to line up the probabilities pointwise which doesn't seem too appetizing right now with the FIniteRange generalization (hopefully I'm overthinking this)

[llllvvuu]

Basically the proof I have in mind is:

$P((\pi(X), U_H) = (H + x, h)) = \sum_{h'} P((X, U_H) = (x + h', h))$
$P(X - U_H = x) = \sum_{h'} P((X, U_H) = (x + h', h + h'))$

Here one sum ranges over $(G / H) \times H$ and another ranges over $G$ and the terms have to be lined up, which I may not be familiar enough with the cosets API to do

[Terence Tao]

llllvvuu said:

I poked at B.3 (ent_of_proj_le) a bit: https://github.com/teorth/pfr/pull/175/files

Currently, H[X - U_H] = H[pi(X), U_H] seeems to be the tedious part because X - U_H and pi(X), U_H marginalize over X, U_H slightly differently so we can't just plug in entropy_eq_of_injective or similar. I think we have to actually manipulate the sum to line up the probabilities pointwise which doesn't seem too appetizing right now with the FIniteRange generalization (hopefully I'm overthinking this)

It should be enough to prove that H[X - UH | π X ] = H[UH]. This in turn should follow from IsUniform ( X-UH | (π X)⁻¹' {y} ) π⁻¹' {y} (the notation may not be exactly this)

[Terence Tao]

The uniformity might be easiest to prove directly from our definition of IsUniform (that every point in π⁻¹' {y} gets the same probability, and the complement of this set gets zero probability)

[Terence Tao]

But yeah it's more of a slog than I first realized... these "obvious" computations are surprisingly lengthy sometimes to formalize

[Terence Tao]

Hmm here is an approach that does not explicitly require checking uniformity. Firstly
$H[X - U_H] = H[X -U_H, \pi(X - U_H)] = H[X-U_H, \pi(X)] = H[X-U_H|\pi(X)] + H[\pi(X)]$
and by independence
$H[U_H, \pi(X)] = H[U_H] + H[\pi(X)]$
while by submodularity and independence
$H[X-U_H|\pi(X)] \geq H[X-U_H|X] = H[U_H|X] = H[U_H] = \log |H|$
but on the other hand, for any $y \in G/H$, $X-U_H$ is supported in $\pi^{-1}(\{y\})$ when $\pi(X) = y$ hence
$H[X-U_H|\pi(X)=y] \leq \log \# \pi^{-1}(\{y\}) = \log |H|$
and thus
$H[X-U_H|\pi(X)] \leq \log |H|.$
The claim now follows from linarith. Still not a short proof, but less computation than some other alternatives.

[Thomas Bloom]

Mauricio Collares said:

I also have a mathematical question regarding PFR_projection

OK, fixed on the blueprint now, but so you don't have to wait for the approval: the only change is that the $\lvert H\rvert$ becomes some unspecified integer $k\geq 0$. The only role is plays is as a bookkepping device, so it doesn't matter if it's unrelated to $H$ otherwise, as long as it's the same integer in both the second and third conditions on maximality.

This should only need a minor adaptation to the proof you've written so far, I'd hope.

[llllvvuu]

Thanks @Terence Tao ! The proof state is much better now. There are slightly tedious side conditions left of course but I'll go ahead and claim this (B.3) as it seems tractable from here

[Mauricio Collares]

@Thomas Bloom Thanks! I'm still a bit confused, though. For proving the upper bound on $\log |H''|$, we would need to show that $\log |H| + \log |H'| \leq (2 - 2 ^{2-k}) (\mathbb{H}(X) + \mathbb{H}(Y))$, but the upper bound we have on $\log |H|$ doesn't seem to leave any "slack" for this; if I understand correctly, the bounds we'd have in this new context are $\log |H| \leq (2 - 2 ^{2-k}) (\mathbb{H}(X) + \mathbb{H}(Y))$ and $\log |H'| < \mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y)) \leq 2^{1-k} (\mathbb{H}(X) + \mathbb{H}(Y))$, and summing we only get a bound of $(2 - 2 ^{1-k}) (\mathbb{H}(X) + \mathbb{H}(Y))$.

[Thomas Bloom]

Right, but that's exactly the bound we want (note $k$ has become $k+1$) since it matches with $H(\psi''(X))+H(\psi''(Y))\leq 2^{-k}(H(X)+H(Y))$.

[Mauricio Collares]

Ah, sorry, I understand now! We're taking $H$ maximal for the property that there exists a $k$ such that $\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))> 44d[\psi(X);\psi(Y)]$, $\log \lvert H\rvert \leq \left(2-2^{2-k}\right)(\mathbb{H}(X)+\mathbb{H}(Y))$ and $\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))\leq 2^{1-k}(\mathbb{H}(X)+\mathbb{H}(Y))$. I had misunderstood the fix at first, thanks!

[Mauricio Collares]

Adapting the proof was indeed very easy, thanks for the very short fix! Still have a bunch of unrelated cleanup to do...

Edit: Submitted as https://github.com/teorth/pfr/pull/176

[llllvvuu]

ent_of_proj_le (B.3) is done: https://github.com/teorth/pfr/pull/175

[Terence Tao]

image.png
weak_pfr_int is now sorry-free! Thanks to everyone who pushed it over the finish line, this was definitely a team effort.

[Sébastien Gouëzel]

Thomas Bloom said:

OK, fixed on the blueprint now.

Looks like the blueprint still holds the old version, am I missing something?

Also, I've PRed a trivial improvement of constants (from 44 to 40) in https://github.com/teorth/pfr/pull/178.

[Mauricio Collares]

I think @Thomas Bloom pushed it to https://github.com/TFBloom/pfr/tree/patch-2 but didn't create a PR. That being said, there's a very minor simplification that can be done on the fixed version: $2^{1-k}$ can be replaced by a non-negative real number $\alpha$, as in https://github.com/teorth/pfr/pull/179

[Sébastien Gouëzel]

Oops, I was working on yet another improvement of the constant (from 40 to 34), by being more precise in the proof that your PR simplifies (see https://github.com/teorth/pfr/pull/180), so there will be a conflict here. Do you think your cleanup would also apply to the version in my PR? (Probably yes!)

[Mauricio Collares]

@Sébastien Gouëzel Nice! I see you also did a lot of cleanup in the calc blocks. I wouldn't mind if you reverted my changes. I like the new argument, and I can always submit a follow-up PR later if I find an analogous simplification.

[Mauricio Collares]

I just checked that replacing α^k by xin your proof still works fine, but I still have to think if it counts as a simplification in this new set-up.

[Mauricio Collares]

I think replacing α^k by x would decrease the readability of your proof. Feel free to fully revert my commit in your version.

[Sébastien Gouëzel]

I've fixed the conflicts in my PR, and borrowed in particular your trick of replacing $\alpha^k$ with an arbitrary constant, both in the Lean file and the blueprint.

[Sébastien Gouëzel]

I've updated the blueprint using a mildly standard latex command (\qedhere), which apparently plastex doesn't know, and is ugly just above https://teorth.github.io/pfr/blueprint/sect0011.html#pfr-projection. @Patrick Massot, should I just remove it (after all, it only changes the appearance of the generated pdf file, which no-one will ever look at anyway), or is there a better way?

[Patrick Massot]

What you see is not plasTeX being confused, it is mathjax being confused.

[Patrick Massot]

See https://math.meta.stackexchange.com/questions/3582/qed-for-mathjax-here-on-stackexchange

[Sébastien Gouëzel]

To me it's both plasTeX and mathjax being confused: \qedhere is a command moving the end of proof symbol around, which doesn't make sense in an html context, so plasTeX should strip it away if it knew what this means. And mathjax should also ignore it, in an ideal world. Anyway, it's really minor!

[Eric Rodriguez]

I'm going on holiday tomorrow and I still haven't had time to do my claim. I'm very happy to still do it later but if anyone wants some work to do, please feel free to take it - I've hogged it for nearly a month now and I feel awful!

[llllvvuu]

I can take a look.

[llllvvuu]

OK, I got it sorry-free: https://github.com/teorth/pfr/pull/182

I also fixed a typo (I think) in the blueprint, I guess $L = C_1C_3 K^{2(C_2+C_4)}$ was meant to cover $A$, but we only need to cover $A'$ (hence $L = C_3 K^{2C_4}$)

[llllvvuu]

BTW, the Zulip PDF link in the proof of 10.3 (bsg) gives me an access denied error; is it worth re-uploading somewhere else?

[Terence Tao]

llllvvuu said:

BTW, the Zulip PDF link in the proof of 10.3 (bsg) gives me an access denied error; is it worth re-uploading somewhere else?

ok, I've hosted it on a new link https://terrytao.files.wordpress.com/2024/01/simplebsg.pdf