Helper lemma for (conditional) Ruzsa distance

Stream: Polynomial Freiman-Ruzsa conjecture

[Paul Lezeau]

In the proof of the Bound on distance increments, one needs to show that $d[X_2^0; W' | S] = d[X_2^0; W' | S]$ where $X_i, X_i' : \Omega \to G$ are random variables, $W = X_1 + X_1'$, $W' = X_2 + X_2'$ and $S = W + W'$.

Edit: $X_2^0$ is some $G$-valued random variable.

The proof mentions this might require a helper lemma for Ruzsa distances, which I am guessing is something of the form

lemma ruzsa_helper_lemma {A B C : Ω → G} {X :  Ω'  → G}
  (hB : Measurable B) (hC : Measurable C) (hA : Measurable A)
  (H : A = B + C) : d[X # B | A] = d[X # C | A]

(with some extra assumptions about e.g. measurability).

My attempts at proving this so far have relied on using cond_rdist'_eq_sum, but I haven't been able to make much progress past that point. Would anyone have some suggestions on which parts of the API I should be working with?

[Arend Mellendijk]

I think some variant of pfr#cond_rdist_of_inj_map for cond_rdist'is what you're looking for. I think you can deduce the half-dependent version from the dependent version with pfr#cond_rdist_of_const (though that might come with a non-empty assumption)

[Paul Lezeau]

Thanks for the advice, I'll have a go at that!

[Rémy Degenne]

@Paul Lezeau would an independence hypothesis be fine in your helper lemma? Also, would it be sufficient for your use case if X has the same type as A,B and C? If yes, here is an almost complete proof:

lemma ruzsa_helper_lemma'
    [IsProbabilityMeasure (ℙ : Measure Ω)] {X B C : Ω → G}
    (hX : Measurable X) (hB : Measurable B) (hC : Measurable C)
    (h_indep : IndepFun X (⟨B, C⟩)) :
    d[X # B | B + C] = d[X # C | B + C] := by
  let π : G × G →+ G :=
  { toFun := fun x ↦ x.2 - x.1
    map_zero' := by simp
    map_add' := fun a b ↦ by simp only [Prod.snd_add, Prod.fst_add,
      ElementaryAddCommGroup.sub_eq_add]; abel }
  let Y : Fin 4 → Ω → G := ![-X, C, fun ω ↦ 0, B + C]
  have hY_meas : ∀ i, Measurable (Y i) := by sorry
  calc d[X # B | B + C]
    = d[X | fun ω : Ω ↦ (0 : G) # B | B + C] := by rw [cond_rdist_of_const hX]
  _ = d[π ∘ ⟨-X, fun ω : Ω ↦ (0 : G)⟩ | fun ω : Ω ↦ (0 : G) # π ∘ ⟨C, B + C⟩ | B + C] := by
        congr
        · ext1 ω; simp
        · ext1 ω
          simp only [AddMonoidHom.coe_mk, ZeroHom.coe_mk, Function.comp_apply, Pi.add_apply]
          abel
  _ = d[π ∘ ⟨Y 0, Y 2⟩ | Y 2 # π ∘ ⟨Y 1, Y 3⟩ | Y 3] := by congr
  _ = d[-X | fun ω : Ω ↦ (0 : G) # C | B + C] := by
        rw [cond_rdist_of_inj_map' _ _ hY_meas π (fun _ ↦ sub_right_injective)]
        · congr
        · sorry -- ⊢ IndepFun (⟨Y 0, Y 2⟩) (⟨Y 1, Y 3⟩) -- deduce it from h_indep
  _ = d[-X # C | B + C] := by rw [cond_rdist_of_const]; exact hX.neg
  _ = d[X # C | B + C] := by -- because ElementaryAddCommGroup G 2
        congr
        simp

cond_rdist_of_inj_map' is the generalization of cond_rdist_of_inj_map with π : G × G →+ G' for some other group G' instead of the special case π : G × G →+ G × G we have now (and in the code above G' = G). If the added assumptions are fine for the use you want to make of the lemma, I'll PR that.

[Rémy Degenne]

By the way I have no idea how to prove the measurability goal about Y because I don't know how to get to 4 goals corresponding to i=0, i=1,i=2 and i=3. I never work with Fin. How would I do that?

[Damiano Testa]

Does fin_cases i help?

[Rémy Degenne]

Yes, that's exactly what I was looking for. Thanks!

[Paul Lezeau]

Rémy Degenne said:

Paul Lezeau would an independence hypothesis be fine in your helper lemma? Also, would it be sufficient for your use case if X has the same type as A,B and C? If yes, here is an almost complete proof:

lemma ruzsa_helper_lemma'
    [IsProbabilityMeasure (ℙ : Measure Ω)] {X B C : Ω → G}
    (hX : Measurable X) (hB : Measurable B) (hC : Measurable C)
    (h_indep : IndepFun X (⟨B, C⟩)) :
    d[X # B | B + C] = d[X # C | B + C] := by
  let π : G × G →+ G :=
  { toFun := fun x ↦ x.2 - x.1
    map_zero' := by simp
    map_add' := fun a b ↦ by simp only [Prod.snd_add, Prod.fst_add,
      ElementaryAddCommGroup.sub_eq_add]; abel }
  let Y : Fin 4 → Ω → G := ![-X, C, fun ω ↦ 0, B + C]
  have hY_meas : ∀ i, Measurable (Y i) := by sorry
  calc d[X # B | B + C]
    = d[X | fun ω : Ω ↦ (0 : G) # B | B + C] := by rw [cond_rdist_of_const hX]
  _ = d[π ∘ ⟨-X, fun ω : Ω ↦ (0 : G)⟩ | fun ω : Ω ↦ (0 : G) # π ∘ ⟨C, B + C⟩ | B + C] := by
        congr
        · ext1 ω; simp
        · ext1 ω
          simp only [AddMonoidHom.coe_mk, ZeroHom.coe_mk, Function.comp_apply, Pi.add_apply]
          abel
  _ = d[π ∘ ⟨Y 0, Y 2⟩ | Y 2 # π ∘ ⟨Y 1, Y 3⟩ | Y 3] := by congr
  _ = d[-X | fun ω : Ω ↦ (0 : G) # C | B + C] := by
        rw [cond_rdist_of_inj_map' _ _ hY_meas π (fun _ ↦ sub_right_injective)]
        · congr
        · sorry -- ⊢ IndepFun (⟨Y 0, Y 2⟩) (⟨Y 1, Y 3⟩) -- deduce it from h_indep
  _ = d[-X # C | B + C] := by rw [cond_rdist_of_const]; exact hX.neg
  _ = d[X # C | B + C] := by -- because ElementaryAddCommGroup G 2
        congr
        simp

cond_rdist_of_inj_map' is the generalization of cond_rdist_of_inj_map with π : G × G →+ G' for some other group G' instead of the special case π : G × G →+ G × G we have now (and in the code above G' = G). If the added assumptions are fine for the use you want to make of the lemma, I'll PR that.

Oh wow that looks great! In my case assuming some independence should be fine. I would however need $X$ to be defined on a different type - would that modification be troublesome?

[Rémy Degenne]

I just finished the adaptation to different spaces. I'll PR it now.

[Paul Lezeau]

Rémy Degenne said:

I just finished the adaptation to different spaces. I'll PR it now.

Ah wonderful I think that's exactly what I need! Thanks so much!

[Rémy Degenne]

https://github.com/teorth/pfr/pull/122