rho_PFR_conjecture

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