\begin{proposition} \label{pfr-rho}\lean{rho_PFR_conjecture}\leanok For any random variables $Y_1,Y_2$, there exist a subgroup $H$ such that
  $$ 2\rho(U_H) \leq \rho(Y_1) + \rho(Y_2) + 8 d[Y_1;Y_2].$$
\end{proposition}
\begin{proof}\leanok
  \uses{phi-min-exist, phi-minimizer-zero-distance,phi-min-def,rho-invariant,sym-zero}
Let $X_1,X_2$ be a $\phi$-minimizer. By \Cref{phi-minimizer-zero-distance} $d[X_1;X_2]=0$, which by \Cref{phi-min-def} implies $\rho(X_1)+\rho(X_2)\le \rho(Y_1) + \rho(Y_2) + \frac{1}{\eta} d[Y_1;Y_2]$ for every $\eta<1/8$. Take the limit at $\eta=1/8$ to get $\rho(X_1)+\rho(X_2)\le \rho(Y_1) + \rho(Y_2) + 8 d[Y_1;Y_2]$.
By \Cref{ruzsa-triangle} and \Cref{ruzsa-nonneg} we have $d[X_1;X_1]=d[X_2;X_2]=0$, and by \Cref{sym-zero} there are $H_1:=\mathrm{Sym}[X_1],H_2:=\mathrm{Sym}[X_2]$ such that $X_1=U_{H_1}+x_1$ and $X_2=U_{H_2}+x_2$ for some $x_2$.
By \Cref{rho-invariant} we get $\rho(U_{H_1})+\rho(U_{H_2})\le \rho(Y_1) + \rho(Y_2) + 8 d[Y_1;Y_2]$, and thus the claim holds for $H=H_1$ or $H=H_2$.
\end{proof}
theorem rho_PFR_conjecture [MeasurableSpace G] [DiscreteMeasurableSpace G]
    (Y₁ Y₂ : Ω → G) (hY₁ : Measurable Y₁) (hY₂ : Measurable Y₂) (A : Finset G) (hA : A.Nonempty) :
    ∃ (H : Submodule (ZMod 2) G) (Ω' : Type uG) (mΩ' : MeasureSpace Ω') (U : Ω' → G),
    IsProbabilityMeasure (ℙ : Measure Ω') ∧ Measurable U ∧
    IsUniform H U ∧ 2 * ρ[U # A] ≤ ρ[Y₁ # A] + ρ[Y₂ # A] + 8 * d[Y₁ # Y₂] := by
  obtain ⟨Ω', mΩ', X₁, X₂, hX₁, hX₂, hP, htau_min, hdist⟩ := phiMinimizer_exists_rdist_eq_zero hA
  wlog h : ρ[X₁ # A] ≤ ρ[X₂ # A] generalizing X₁ X₂
  · rw [rdist_symm] at hdist
    exact this X₂ X₁ hX₂ hX₁ (phiMinimizes_comm htau_min) hdist (by linarith)
  -- use for `U` a translate of `X` to make sure that `0` is in its support.
  obtain ⟨x₀, h₀⟩ : ∃ x₀, ℙ (X₁⁻¹' {x₀}) ≠ 0 := by
    by_contra! h
    have A a : (ℙ : Measure Ω').map X₁ {a} = 0 := by
      rw [Measure.map_apply hX₁ .of_discrete]
      exact h _
    have B : (ℙ : Measure Ω').map X₁ = 0 := by
      rw [← Measure.sum_smul_dirac (μ := (ℙ : Measure Ω').map X₁)]
      simp [A]
    have : IsProbabilityMeasure ((ℙ : Measure Ω').map X₁) :=
      isProbabilityMeasure_map hX₁.aemeasurable
    exact IsProbabilityMeasure.ne_zero _ B
  have h_unif : IsUniform (symmGroup X₁ hX₁) (fun ω ↦ X₁ ω - x₀) := by
    have h' : d[X₁ # X₁] = 0 := by
      apply le_antisymm _ (rdist_nonneg hX₁ hX₁)
      calc
        d[X₁ # X₁] ≤ d[X₁ # X₂] + d[X₂ # X₁] := rdist_triangle hX₁ hX₂ hX₁
        _ = 0 := by rw [hdist, rdist_symm, hdist, zero_add]
    exact isUniform_sub_const_of_rdist_eq_zero hX₁ h' h₀
  refine ⟨AddSubgroup.toZModSubmodule 2 (symmGroup X₁ hX₁), Ω', by infer_instance,
    fun ω ↦ X₁ ω - x₀, by infer_instance, by fun_prop, by exact h_unif, ?_⟩
  have J : d[X₁ # X₂] + (1/8) * (ρ[X₁ # A] + ρ[X₂ # A])
      ≤ d[Y₁ # Y₂] + (1/8) * (ρ[Y₁ # A] + ρ[Y₂ # A]) := by
    have Z := le_rdist_of_phiMinimizes htau_min hY₁ hY₂ (μ₁ := ℙ) (μ₂ := ℙ)
    linarith
  rw [hdist, zero_add] at J
  have : ρ[fun ω ↦ X₁ ω - x₀ # A] = ρ[X₁ # A] := by
    simp_rw [sub_eq_add_neg, rho_of_translate hX₁ hA]
  linarith

/-- If $|A+A| \leq K|A|$, then there exists a subgroup $H$ and $t\in G$ such that
$|A \cap (H+t)| \geq K^{-4} \sqrt{|A||V|}$, and $|H|/|A|\in[K^{-8},K^8]$. -/