Ruzsa triangle inequality

Stream: Polynomial Freiman-Ruzsa conjecture

[Paul Lezeau]

Hi! Following a small chat with Yaël, I'd like to claim ruzsa-triangle

[Rémy Degenne]

Does that include ent_of_diff_le? If so, here is my progress so far:

/-- The improved Ruzsa triangle inequality -/
lemma ent_of_diff_le (X : Ω → G) (Y : Ω → G) (Z : Ω → G)
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    (h : IndepFun (⟨ X, Y ⟩) Z μ) [IsProbabilityMeasure μ] :
    H[X - Y; μ] ≤ H[X - Z; μ] + H[Z - Y; μ] - H[Z; μ] := by
  have h1 : H[⟨X - Z, ⟨Y, X - Y⟩⟩; μ] + H[X - Y; μ] ≤ H[⟨X - Z, X - Y⟩; μ] + H[⟨Y, X - Y⟩; μ] :=
    entropy_triple_add_entropy_le μ (hX.sub hZ) hY (hX.sub hY)
  have h2 : H[⟨X - Z, X - Y⟩ ; μ] ≤ H[X - Z ; μ] + H[Y - Z ; μ] := by
    calc H[⟨X - Z, X - Y⟩ ; μ] ≤ H[⟨X - Z, Y - Z⟩ ; μ] := by
          have : ⟨X - Z, X - Y⟩ = (fun p ↦ (p.1, p.1 - p.2)) ∘ ⟨X - Z, Y - Z⟩ := by ext1; simp
          rw [this]
          exact entropy_comp_le μ ((hX.sub hZ).prod_mk (hY.sub hZ)) (measurable_of_finite _)
    _ ≤ H[X - Z ; μ] + H[Y - Z ; μ] := by
          have h : 0 ≤ H[X - Z ; μ] + H[Y - Z ; μ] - H[⟨X - Z, Y - Z⟩ ; μ] :=
            mutualInformation_nonneg (hX.sub hZ) (hY.sub hZ) μ
          linarith
  have h3 : H[⟨ Y, X - Y ⟩ ; μ] ≤ H[⟨ X, Y ⟩ ; μ] := by
    have : ⟨Y, X - Y⟩ = (fun p ↦ (p.2, p.1 - p.2)) ∘ ⟨X, Y⟩ := by ext1;  simp
    rw [this]
    exact entropy_comp_le μ (hX.prod_mk hY) (measurable_snd.prod_mk measurable_sub)
  have h4 : H[⟨X - Z, ⟨Y, X - Y⟩⟩; μ] = H[⟨X, ⟨Y, Z⟩⟩ ; μ] := by
    refine entropy_of_comp_eq_of_comp μ ((hX.sub hZ).prod_mk (hY.prod_mk (hX.sub hY)))
      (fun p : G × (G × G) ↦ (p.2.2 + p.2.1, p.2.1, -p.1 - p.2.2 - p.2.1))
      (fun p : G × G × G ↦ (p.1 - p.2.2, p.2.1, p.1 - p.2.1)) ?_ ?_
    · sorry
    · sorry
  have h5 : H[⟨X, ⟨Y, Z⟩⟩ ; μ] = H[⟨X, Y⟩ ; μ] + H[Z ; μ] := by
    rw [entropy_assoc hX hY hZ, entropy_pair_eq_add (hX.prod_mk hY) hZ]
    exact h
  rw [h4, h5] at h1
  calc H[X - Y; μ] ≤ H[X - Z; μ] + H[Y - Z; μ] - H[Z; μ] := by linarith
  _ = H[X - Z; μ] + H[Z - Y; μ] - H[Z; μ] := by
    congr 2
    rw [entropy_sub_comm hY hZ]

[Rémy Degenne]

I'm happy to let you continue from here if you wish. The h1, h2... correspond to the steps detailed in the blueprint.

[Paul Lezeau]

Oh I was just going to have a go at rdist_triangle for starters!

[Paul Lezeau]

I don't want to steal your work!

[Rémy Degenne]

Ok. I have continued working on it (and updated the code above). The two sorry left should be trivial but I am having difficulties with the prod abbreviation introduced in the project. simp does not see through it. (I misunderstood my code and that was not the issue)

Also the independence hypothesis I used is not the same as in the blueprint: I have (X,Y) independent of Z, while https://teorth.github.io/pfr/blueprint/sect0003.html#ruzsa-triangle-improved is stated with (X,Z) independent of Y. Is that a typo, or did I prove the wrong thing?

[Rémy Degenne]

PR for this: https://github.com/teorth/pfr/pull/48

[Terence Tao]

Rémy Degenne said:

Ok. I have continued working on it (and updated the code above). The two sorry left should be trivial but I am having difficulties with the prod abbreviation introduced in the project. simp does not see through it. (I misunderstood my code and that was not the issue)

Also the independence hypothesis I used is not the same as in the blueprint: I have (X,Y) independent of Z, while https://teorth.github.io/pfr/blueprint/sect0003.html#ruzsa-triangle-improved is stated with (X,Z) independent of Y. Is that a typo, or did I prove the wrong thing?

Oops, that was indeed a typo. I'll get it changed when I get back to a machine with access to the repo. (For the application to the Ruzsa distance inequality, all three variables can be made independent of each other, so the typo doesn't much matter for this project.) Technically I guess this is the first discovery of an error arising from the formalization project - a milestone of sorts, I guess! (But one that came from the blueprint, not the paper, which only states the inequality assuming all three variables independent.)

[Terence Tao]

Paul Lezeau said:

Oh I was just going to have a go at rdist_triangle for starters!

Welcome to the project! I think this is quite a doable lemma now with all the prerequisites (and also examples of similar lemmas already been proven).

More generally, most of the lemmas in https://teorth.github.io/pfr/blueprint/sect0003.html should now be within reach, except possibly for some involving conditional Ruzsa distance where we don't yet have a formal definition (but even then, some of the later lemmas about conditional Ruzsa distance might be derivable from the earlier lemmas at this current stage). The fibring identities in https://teorth.github.io/pfr/blueprint/sect0005.html are also somewhat similar to the Ruzsa triangle inequality and the Kaimonovich-Vershik inequality and should also be manageable now.

The most difficult entropic Ruzsa distance inequality is the Balog-Szemeredi-Gowers lemma, which isn't even formalized right now (it involves a conditioning to Z ← z). I think if we get a bit more experience formalizing the rest of the entropic distance inequalities, though, it will be clear how to do this one also. Formalising this lemma would, roughly speaking, mark the halfway point in this project, I think.

[Yaël Dillies]

FWIW @Bhavik Mehta and I are thinking about BSG (but not only the entropic version).

[Paul Lezeau]

Completed at https://github.com/teorth/pfr/pull/60

[Rémy Degenne]

You also pushed your lake-manifest.json file to the branch of that pr. Could you undo that change ?

[Paul Lezeau]

Rémy Degenne said:

You also pushed your lake-manifest.json file to the branch of that pr. Could you undo that change ?

I'll do that now!

[Paul Lezeau]

Done!