Outstanding tasks, version 3.0

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

Seems like the "outstanding tasks" list needs to refresh every 48 hours or so. Here is the new list. The previous thread can be found here.

Existing claims:

1. @Jonas Bayer, @llllvvuu , and @Paul Lezeau are working on Bounded entropy implies concentration, though not quite with a complete proof yet.
2. @Yaël Dillies and @Bhavik Mehta claim Entropic Balog-Szemeredi-Gowers
3. @Rémy Degenne has partially established Alternate form of distance
4. @Aaron Anderson has established Special case of Fibring identity
5. @Paul Lezeau claims Entropy of uniform random variable
6. @Sebastien Gouezel has almost established Polynomial Freiman-Ruzsa conjecture

Outstanding tasks:

1. Symmetry identity This should follow from Copy preserves entropy and definitions; some partial progress had already been made on this by @Kyle Miller, but more remains to be done.
2. Existence of conditionally independent trials This is a variant of Existence of independent copies that is needed for the Balog-Szemeredi-Gowers lemma (so it may make sense for whoever is working on this to coordinate with Yael and Bhavik on this). Established by @Terence Tao
3. Fibring identity for first estimate This should be an immediate application of Special case of Fibring identity Established by @Arend Mellendijk
4. First estimate This should be a linear combination of existing inequalities. Established by @Rob Lewis
5. Entropy bound on quadruple sum This should be a linear combination of existing inequalities. Completed by @Kalle Kytölä and @Mantas Baksys .
6. Conditional distance lower bound This inequality should follow from applying definition of conditional distance and then averaging Distance lower bound. Established by @Terence Tao
7. Bound on distance increments This should be a straightforward linear combination of Entropy bound on quadruple sum and Comparison of Ruzsa distances, II
8. Distance between sums - This should be a routine linear combination of Distance lower bound and Comparison of Ruzsa distances, I. Established by @Ben Eltschig
9. Second estimate This is a linear combination of existing inequalities. Claimed by @Ben Eltschig
10. tau decrement This combines a number of difficult estimates to produce a new pair of random variables with a smaller tau-functional than the initial pair. While this is a substantial result in the paper, the derivation from previous lemmas is relatively straightforward and this result may only be of moderate difficulty to formalize. Claimed by @Arend Mellendijk
11. Constructing good variables. I This is a technical inequality that is currently blocked due to the lack of formalization of Entropic Balog-Szemeredi-Gowers. It is a moderately complicated linear combination of previous inequalities.
12. Constructing good variables, II This is obtained by averaging Constructing good variables. I over 3!=6 permutations. Completed by @Rob Lewis

Making good progress - at this rate we should be largely done by the end of next week!

[Yaël Dillies]

Bhavik and I are still pondering about the proof. We'll start actually writing Lean code next Thursday.

[Rob Lewis]

Here is 4. A very easy one from a bystander! It's fun watching this come together.

[Terence Tao]

Yaël Dillies said:

Bhavik and I are still pondering about the proof. We'll start actually writing Lean code next Thursday.

OK, good to know. If you are able to write down a statement of entropic BSG before that date, that would unblock item 11 as well, which would be helpful.

[Arend Mellendijk]

Here's 3

[Terence Tao]

I'm going to go ahead and claim 2.

EDIT: This is now done, though it was lengthier than I expected.

[Ben Eltschig]

8 should be done as well now with #79

[Ben Eltschig]

I'll try doing the second estimate tomorrow, if no one else has claimed it by then

[Kalle Kytölä]

I could try to fill in (5) entropy bound on quadruple sums (i.e. I'd like to claim it for a while).

[Kalle Kytölä]

I think I'll have to call it a day. The missing part towards quadruple sums is the "obvious" lemma below, I'll PR the rest. Thanks a lot also to @Mantas Baksys for sharing work.

So I will not currently claim the remaining part of the quadruple sums (which is the lemma below). But if no one picks this up, I could try to fill in the remaining sorry tomorrow evening.

lemma sum_sum_indep_of_iIndep (h_indep : iIndepFun (fun _i => hG) ![X₁, X₂, X₂', X₁']) :
    IndepFun (X₁ + X₂') (X₂ + X₁') := by
  sorry

[Terence Tao]

Kalle Kytölä said:

I think I'll have to call it a day. The missing part towards quadruple sums is the "obvious" lemma below, I'll PR the rest. Thanks a lot also to Mantas Baksys for sharing work.

So I will not currently claim the remaining part of the quadruple sums (which is the lemma below). But if no one picks this up, I could try to fill in the remaining sorry tomorrow evening.

lemma sum_sum_indep_of_iIndep (h_indep : iIndepFun (fun _i => hG) ![X₁, X₂, X₂', X₁']) :
    IndepFun (X₁ + X₂') (X₂ + X₁') := by
  sorry

Thanks for the update! We already have the tool pfr#ProbabilityTheory.iIndepFun.indepFun_prod_prod that another contributor helpfully wrote up which could be useful here... hopefully one just has to combine it with docs#ProbabilityTheory.IndepFun.comp ?

[llllvvuu]

Hi everyone, I saw prob_ge_exp_neg_entropy on Twitter and jumped in to try it in order to learn Lean. I didn't realize it was already claimed by @Jonas Bayer so I'll close off here for now (this is fun though)

Here's what I came up with if it helps (now that I look at it, contradiction would be much shorter): https://github.com/llllvvuu/pfr/blob/e625ed53746919b82692a2e794e5289c401bcc7f/PFR/Entropy/Basic.lean#L278-L342

[Paul Lezeau]

Yeah I also accidentally proved that one (I misread the list of claimed lemmas) - I have a sorry free version locally :grimacing:

[Sebastien Gouezel]

Deducing combinatorial PFR from entropic PFR is essentially done in https://github.com/teorth/pfr/pull/83 (two sorries remaining, but they have nothing to do with the main line of the argument).

[Terence Tao]

Paul Lezeau said:

Yeah I also accidentally proved that one (I misread the list of claimed lemmas) - I have a sorry free version locally :grimacing:

Oops! Well, I guess it happens, and we can't actually prevent people from working to prove whatever they like, and having multiple proofs for the same result happens all the time in unformalized mathematics as well. @Jonas Bayer , how far are you along in your formalization? Depending on the situation, we could try to merge the different attempts, or help you complete any missing gaps in the argument.

[Terence Tao]

Sebastien Gouezel said:

Deducing combinatorial PFR from entropic PFR is essentially done in https://github.com/teorth/pfr/pull/83 (two sorries remaining, but they have nothing to do with the main line of the argument).

That's great progress! Are you planning to close off these sorries yourself, or would you prefer to return them to the list of outstanding tasks? If the latter, then it may make sense to write them as standalone lemmas (and perhaps also update the blueprint accordingly).

[Sebastien Gouezel]

Sebastien Gouezel said:

Deducing combinatorial PFR from entropic PFR is essentially done in https://github.com/teorth/pfr/pull/83 (two sorries remaining, but they have nothing to do with the main line of the argument).

By the way, the finiteness assumption of G can be removed from the final theorem, for stupid reasons: an infinite set c satisfies Nat.card c = 0, so taking c = G and H = {0} works when the group is infinite. Not so interesting mathematically, though :-)

I guess it can also be removed in a more reasonable way by adding the conclusion that c is finite (by taking the subgroup spanned by A, which is finite, and working there).

[Sebastien Gouezel]

Terence Tao said:

Sebastien Gouezel said:
That's great progress! Are you planning to close off these sorries yourself, or would you prefer to return them to the list of outstanding tasks? If the latter, then it may make sense to write them as standalone lemmas (and perhaps also update the blueprint accordingly).

I'll try to close them off. I'm less familiar with this part of mathlib, but hopefully it shouldn't be hard.

[Terence Tao]

Sebastien Gouezel said:

Sebastien Gouezel said:

Deducing combinatorial PFR from entropic PFR is essentially done in https://github.com/teorth/pfr/pull/83 (two sorries remaining, but they have nothing to do with the main line of the argument).

By the way, the finiteness assumption of G can be removed from the final theorem, for stupid reasons: an infinite set c satisfies Nat.card c = 0, so taking c = G and H = {0} works when the group is infinite. Not so interesting mathematically, though :-)

I guess it can also be removed in a more reasonable way by adding the conclusion that c is finite (by taking the subgroup spanned by A, which is finite, and working there).

We could perhaps add a PFR_conjecture' corollary that removes the finiteness hypothesis on G and instead imposes finiteness on c (and H) as you suggest and add it to the blueprint and list of outstanding tasks. It seems like a fairly straightforward derivation from PFR_conjecture; the trickiest things I see are to verify that every finite set in an elementary 2-group generates a finite group, and to handle the various coercions between subsets of a subgroup and subsets of the whole group (the latter is not fundamentally difficult, but it still trips me up sometimes).

[Paul Lezeau]

Terence Tao said:

Paul Lezeau said:

Yeah I also accidentally proved that one (I misread the list of claimed lemmas) - I have a sorry free version locally :grimacing:

Oops! Well, I guess it happens, and we can't actually prevent people from working to prove whatever they like, and having multiple proofs for the same result happens all the time in unformalized mathematics as well. Jonas Bayer , how far are you along in your formalization? Depending on the situation, we could try to merge the different attempts, or help you complete any missing gaps in the argument.

If it helps, here's the formalization I wrote:

lemma Finset.Nonempty_image {α β : Type*} [DecidableEq β]
{s : Finset α} (hs : s.Nonempty) (f : α → β) : (s.image f).Nonempty := by
  rw [Finset.Nonempty] at hs ⊢
  obtain ⟨x, hx⟩ := hs
  use (f x)
  exact Finset.mem_image_of_mem f hx

lemma Finset.image_min'_le_sum {α β : Type*} [DecidableEq β] [LinearOrder β] [AddCommMonoid β]
{s : Finset α} (hs : s.Nonempty) (f : α → β) (hf : ∀ a, 0 ≤ f a ):
  (s.image f).min' (Finset.Nonempty_image hs f) ≤ s.sum f := sorry

lemma Measure.eq_zero_of_map_eq_zero (X : Ω → S) (μ : Measure Ω) (hX : AEMeasurable X μ)
  [NeZero μ] (hμ : μ.map X = 0) : μ = 0 := by
  have := Measure.preimage_null_of_map_null hX (Measure.measure_univ_eq_zero.mpr hμ)
  rwa [preimage_univ, Measure.measure_univ_eq_zero] at this

lemma negIdMulLog_le_neg_log_of_mem_Icc {x : ℝ} (hx : x ∈ Set.Icc 0 1) :
  - log x ≤ negIdMulLog x:= sorry

/-- If $X$ is an $S$-valued random variable, then there exists $s \in S$ such that
$P[X=s] \geq \exp(-H[X])$. -/
lemma prob_ge_exp_neg_entropy [Nonempty S] (X : Ω → S) (hX : Measurable X) (μ : Measure Ω)
  (hμ' : IsFiniteMeasure μ) [NeZero μ] (hbd : ∀ (s : S), μ.map X {s} ≠ 0) :
  ∃ s : S, μ.map X {s} ≥ (μ.map X Set.univ) * (rexp (- H[X ; μ])).toNNReal := by
  -- A few helper lemmas for later
  have nonempty : (Finset.univ.image (fun (x : S) =>
    (-log ((μ.map X Set.univ)⁻¹ * (μ.map X) {x}).toReal))).Nonempty
  · apply Finset.Nonempty_image (Finset.univ_nonempty) _
  haveI := (Measure.isFiniteMeasure_map μ X)
  have pos' : (μ.map X Set.univ) ≠ 0
  · intro h
    have := Measure.preimage_null_of_map_null hX.aemeasurable h
    rw [preimage_univ, Measure.measure_univ_eq_zero] at this
    apply (NeZero.ne μ) this
  have mul_pos : ∀ (s : S), 0 < ((μ.map X Set.univ)⁻¹ * (μ.map X {s})).toReal
  · intro s
    simp only [ENNReal.toReal_mul, gt_iff_lt]
    apply mul_pos (ENNReal.toReal_pos (ENNReal.inv_ne_zero.mpr (measure_ne_top _ _))
      (ENNReal.inv_ne_top.mpr pos')) (ENNReal.toReal_pos (hbd s) (measure_ne_top _ _))
  have prob_mem_Icc : ∀ (s : S), ((μ.map X Set.univ)⁻¹ * ((μ.map X) {s})).toReal ∈ Set.Icc 0 1
  · intro s
    apply (Set.mem_Icc.mpr ⟨ENNReal.toReal_nonneg, _⟩)
    rw [ENNReal.toReal_mul, ENNReal.toReal_inv, inv_mul_le_iff (ENNReal.toReal_pos pos'
      (measure_ne_top _ _)), mul_one, ENNReal.toReal_le_toReal (measure_ne_top _ _) (measure_ne_top _ _)]
    apply measure_mono (by rw [Set.singleton_subset_iff] ; apply Set.mem_univ s)
  -- First notice that H[X] = ∑ s, - ℙ[X = s] log ℙ[X = s] ≥ min - log ℙ[X = s]
  have ineq : H[X ; μ] ≥ (Finset.univ.image (fun (x : S) =>
    (- log ((μ.map X Set.univ)⁻¹ * (μ.map X) {x}).toReal))).min' nonempty
  · calc H[X ; μ] = ∑ x : S, (negIdMulLog (((μ.map X Set.univ)⁻¹ * ((μ.map X) {x})).toReal)) := by
          simp only [entropy_def, measureEntropy_def, Measure.smul_toOuterMeasure,
            OuterMeasure.coe_smul, Pi.smul_apply, smul_eq_mul, ENNReal.toReal_mul]
      _ ≥ ∑ x : S, (- log (((μ.map X Set.univ)⁻¹ * ((μ.map X) {x})).toReal)) :=
           Finset.sum_le_sum (fun i _ => negIdMulLog_le_neg_log_of_mem_Icc (prob_mem_Icc i))
      _ ≥ (Finset.univ.image (fun (x : S) =>
            (- log ((μ.map X Set.univ)⁻¹ * (μ.map X) {x}).toReal))).min' nonempty :=
          Finset.image_min'_le_sum (Finset.univ_nonempty) _ (fun i => neg_nonneg_of_nonpos
          (log_nonpos (Set.mem_Icc.mp (prob_mem_Icc i)).left (Set.mem_Icc.mp (prob_mem_Icc i)).right))
  -- Take s that attains the minimum. This is the element we are after
  obtain ⟨s, _, hs⟩ := (Finset.mem_image.mp (Finset.min'_mem (Finset.univ.image
    (fun (x : S) => (- log ((μ.map X Set.univ)⁻¹ * (μ.map X) {x}).toReal))) nonempty))
  use s
  -- Apply x ↦ exp(- x) on both sides
  rw [←hs, ge_iff_le, ←neg_le_neg_iff, neg_neg] at ineq
  replace ineq := exp_monotone ineq
  -- Rewrite the inequality in terms of ENNReal
  rw [Real.exp_log (mul_pos s), ENNReal.toReal_mul] at ineq
  rw [ge_iff_le, ENNReal.mul_le_iff_le_inv pos' (measure_ne_top _ _), ENNReal.ofNNReal,
    ←ENNReal.toReal_le_toReal _ (ENNReal.mul_ne_top (ENNReal.inv_ne_top.mpr pos') (measure_ne_top _ _)),
    ENNReal.some_eq_coe', ENNReal.coe_toReal, coe_toNNReal',
    ENNReal.toReal_mul, max_le_iff]
  · refine ⟨ineq, by rw [←ENNReal.toReal_mul] ; apply ENNReal.toReal_nonneg⟩
  · apply ENNReal.coe_ne_top

[Kyle Miller]

Pretty printing note: attribute [pp_dot] Measure.map doesn't work correctly since Measure.map doesn't take a Measure as its first explicit argument. This is a limitation of pp_dot.

[Terence Tao]

Ah, so that is what was going on! I was wondering why μ.map X kept pretty printing as X.map μ.

[Paul Lezeau]

I found it quite confusing at first too (especially when copy and pasting from the infoview!)

[Jonas Bayer]

Terence Tao said:

Paul Lezeau said:

Yeah I also accidentally proved that one (I misread the list of claimed lemmas) - I have a sorry free version locally :grimacing:

Oops! Well, I guess it happens, and we can't actually prevent people from working to prove whatever they like, and having multiple proofs for the same result happens all the time in unformalized mathematics as well. Jonas Bayer , how far are you along in your formalization? Depending on the situation, we could try to merge the different attempts, or help you complete any missing gaps in the argument.

I started working on this locally, but haven't completed the proof yet. Since @Paul Lezeau has a complete proof I believe the most natural thing to do would just be to merge his formalization and then focus our effort on the remaining open lemmas.

[Terence Tao]

Jonas Bayer said:

Terence Tao said:

Paul Lezeau said:

Yeah I also accidentally proved that one (I misread the list of claimed lemmas) - I have a sorry free version locally :grimacing:

Oops! Well, I guess it happens, and we can't actually prevent people from working to prove whatever they like, and having multiple proofs for the same result happens all the time in unformalized mathematics as well. Jonas Bayer , how far are you along in your formalization? Depending on the situation, we could try to merge the different attempts, or help you complete any missing gaps in the argument.

I started working on this locally, but haven't completed the proof yet. Since Paul Lezeau has a complete proof I believe the most natural thing to do would just be to merge his formalization and then focus our effort on the remaining open lemmas.

OK, sounds good. Paul, could you set up a PR? Probably there is some way to make the proof shorter (e.g., by working with the contrapositive formulation, and maybe also taking advantage of the methods in MeasureReal to remove some of the ENNReal coercions), but a proof is a proof :). (And anyone can still volunteer to update the proof later if they so choose, even if it might not be listed as a priority item on the outstanding task list any more.)

[Paul Lezeau]

Terence Tao said:

Jonas Bayer said:

Terence Tao said:

Paul Lezeau said:

Yeah I also accidentally proved that one (I misread the list of claimed lemmas) - I have a sorry free version locally :grimacing:

Oops! Well, I guess it happens, and we can't actually prevent people from working to prove whatever they like, and having multiple proofs for the same result happens all the time in unformalized mathematics as well. Jonas Bayer , how far are you along in your formalization? Depending on the situation, we could try to merge the different attempts, or help you complete any missing gaps in the argument.

I started working on this locally, but haven't completed the proof yet. Since Paul Lezeau has a complete proof I believe the most natural thing to do would just be to merge his formalization and then focus our effort on the remaining open lemmas.

OK, sounds good. Paul, could you set up a PR? Probably there is some way to make the proof shorter (e.g., by working with the contrapositive formulation, and maybe also taking advantage of the methods in MeasureReal to remove some of the ENNReal coercions), but a proof is a proof :). (And anyone can still volunteer to update the proof later if they so choose, even if it might not be listed as a priority item on the outstanding task list any more.)

Sure!

[Paul Lezeau]

Here is the PR.

[Kyle Miller]

Terence Tao said:

Ah, so that is what was going on! I was wondering why μ.map X kept pretty printing as X.map μ.

I think this is the right incantation to get it to pretty print as μ.map X rather than Measure.map X μ:

@[app_unexpander Measure.map]
def Measure.map.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $f $μ) => `($(μ).$(Lean.mkIdent `map) $f)
  | _ => throw ()

(Hopefully Lean will have something easier to invoke than this that's more reliable than pp_dot.)

[Kalle Kytölä]

Terence Tao said:

Thanks for the update! We already have the tool pfr#ProbabilityTheory.iIndepFun.indepFun_prod_prod that another contributor helpfully wrote up which could be useful here... hopefully one just has to combine it with docs#ProbabilityTheory.IndepFun.comp ?

Thank you! That's of course right. It was just very late yesterday and I had to stop. I'm PRing this now, so the quadruple sums are sorry-free.

[Terence Tao]

Paul Lezeau said:

Here is the PR.

Hmm, I think there may actually be an issue with the proof, in particular the sorried lemma negIdMulLog_le_neg_log_of_mem_Icc in the PR (claiming $-\log x \leq -x \log x$ for $0 \leq x \leq 1$) looks to be incorrect (the inequality actually goes the other way). I'm not sure that the argument is easily fixable, in which case we may want to return this task to the "outstanding" pile.

[Kalle Kytölä]

Kalle Kytölä said:

Thank you! That's of course right. It was just very late yesterday and I had to stop. I'm PRing this now, so the quadruple sums are sorry-free.

To clarify: not sorry-free globally --- as some prerequisites are still not done. But locally sorry-free.

[Paul Lezeau]

Terence Tao said:

Paul Lezeau said:

Here is the PR.

Hmm, I think there may actually be an issue with the proof, in particular the sorried lemma negIdMulLog_le_neg_log_of_mem_Icc in the PR (claiming $-\log x \leq -x \log x$ for $0 \leq x \leq 1$) looks to be incorrect (the inequality actually goes the other way). I'm not sure that the argument is easily fixable, in which case we may want to return this task to the "outstanding" pile.

Whops that was a silly mistake! I'll fix up the proof now!

[Paul Lezeau]

I've pushed a (hopefully mistake-free!) fix to the PR

[Paul Lezeau]

This has however made the proof a bit longer, so I'll try to shorten it a bit (and prove the extra lemmas I added) now

[Terence Tao]

Paul Lezeau said:

This has however made the proof a bit longer, so I'll try to shorten it a bit (and prove the extra lemmas I added) now

For the remaining lemmas you may find docs#MeasureTheory.measure_biUnion_finset to be useful. I had to prove something a bit similar in https://github.com/teorth/pfr/blob/master/PFR/Entropy/Basic.lean#L1235 (and I got this argument from adapting another contributor's argument in https://github.com/teorth/pfr/blob/master/PFR/Entropy/Basic.lean#L236 ). Eventually it may make sense to make an abstraction of this lemma that could go into https://teorth.github.io/pfr/docs/PFR/Entropy/Measure.html (indeed one could plausibly use pfr#integral_eq_sum here as well).

[Paul Lezeau]

Ah well I've just found out the first one has already been proven!

[Terence Tao]

Paul Lezeau said:

Ah well I've just found out the first one has already been proven!

Ah, right, we already have pfr#sum_measure_singleton and pfr#sum_toReal_measure_singleton (and you inspired me to reroute my own proof of a similar statement through the former, saving a few lines of code). For the other two lemmas you may find the instance in docs#MeasureTheory.isProbabilityMeasureSMul to automatically help with simp etc..

[Arend Mellendijk]

I'm trying my hand at 10 at the moment.

[Terence Tao]

I'm going to try 6.

EDIT: Done

[Rob Lewis]

I was idly poking around at

12. Constructing good variables, II,

which is very straightforward if the $T_i$s are measurable and thus entropy_comm applies. I'm only following things hyper locally -- I think this lemma ends up being applied to measurable things, but I'm not sure (and there may well be a proof that doesn't assume measurability). Am I on the wrong track here?

[Arend Mellendijk]

I can say quite confidently that we only need measurable $T_i$ for this specific lemma. I think people have also generally been assuming measurability throughout.

[Terence Tao]

Rob Lewis said:

I was idly poking around at

12. Constructing good variables, II,

which is very straightforward if the $T_i$s are measurable and thus entropy_comm applies. I'm only following things hyper locally -- I think this lemma ends up being applied to measurable things, but I'm not sure (and there may well be a proof that doesn't assume measurability). Am I on the wrong track here?

We've been careless about inserting measurability hypotheses; at the end of the day, all our random variables are defined on discrete spaces and so measurability is automatic. So if you want to claim 12, please go ahead and insert whatever measurability hypotheses are needed to make the lemma work. (For similar reasons, you may need to assume that various ambient measures are probability measures if needed.)

[Rob Lewis]

Okay! Then, https://github.com/teorth/pfr/pull/92 :smile:

[llllvvuu]

I took some pointers from @Paul Lezeau 's code to fill out my version a bit more: https://github.com/teorth/pfr/pull/94/files

The only remaining assumption is μ Set.univ = μ.map X Set.univ (or replace μ Set.univ in the problem statement)

It definitely needs some refactor/golfing. I could extract some steps to the global scope like what @Paul Lezeau has done, and/or help fill in his lemmas using my logic

[Rémy Degenne]

If you add the hypothesis that X is measurable you can use Measure.map_apply to prove that remaining sorry

[llllvvuu]

Thanks for the tip; the proof compiles now, yay!

(will golf it later - EDIT: actually I might not have enough experience yet with Lean to golf in the near term. will just leave up for comments for now)

[Paul Lezeau]

@llllvvuu since you've opened up a PR too shall I just close mine?

[Paul Lezeau]

I've repurposed the PR to prove IsUniform.entropy_eq