\begin{lemma}[$\phi$-minimizers exist]\label{phi-min-exist}\lean{phi_min_exists}\leanok  There exists a $\phi$-minimizer.
\end{lemma}
\begin{proof}\leanok\uses{rho-cts} Clear from compactness.
\end{proof}
/-- There exists a $\phi$-minimizer. -/
lemma phi_min_exists (hA : A.Nonempty) : ∃ (μ : Measure (G × G)), IsProbabilityMeasure μ ∧
    phiMinimizes Prod.fst Prod.snd η A μ := by
  let _i : TopologicalSpace G := (⊥ : TopologicalSpace G)
  have : DiscreteTopology G := ⟨rfl⟩
  let iG : Inhabited G := ⟨0⟩
  have T : Continuous (fun (μ : ProbabilityMeasure (G × G)) ↦ phi Prod.fst Prod.snd η A μ) := by
    apply continuous_iff_continuousAt.2 (fun μ ↦ ?_)
    apply Tendsto.add
    · apply tendsto_rdist_probabilityMeasure continuous_fst continuous_snd tendsto_id
    apply Tendsto.const_mul
    apply Tendsto.add
    · apply tendsto_rho_probabilityMeasure continuous_fst hA tendsto_id
    · apply tendsto_rho_probabilityMeasure continuous_snd hA tendsto_id
  obtain ⟨μ, _, hμ⟩ := @IsCompact.exists_isMinOn ℝ (ProbabilityMeasure (G × G))
                          _ _ _ _ Set.univ isCompact_univ ⟨default, trivial⟩ _ T.continuousOn
  refine ⟨μ, by infer_instance, ?_⟩
  intro Ω' mΩ' X' Y' hP hX' hY'
  let ν : Measure (G × G) := Measure.map (⟨X', Y'⟩) ℙ
  have : IsProbabilityMeasure ν := isProbabilityMeasure_map (by fun_prop)
  let ν' : ProbabilityMeasure (G × G) := ⟨ν, this⟩
  have : phi Prod.fst Prod.snd η A ↑μ ≤ phi Prod.fst Prod.snd η A ↑ν' := hμ (mem_univ _)
  apply this.trans_eq
  have h₁ : IdentDistrib Prod.fst X' (ν' : Measure (G × G)) ℙ := by
    refine ⟨measurable_fst.aemeasurable, hX'.aemeasurable, ?_⟩
    simp only [ProbabilityMeasure.coe_mk, ν', ν]
    rw [Measure.map_map measurable_fst (by fun_prop)]
    rfl
  have h₂ : IdentDistrib Prod.snd Y' (ν' : Measure (G × G)) ℙ := by
    refine ⟨measurable_snd.aemeasurable, hY'.aemeasurable, ?_⟩
    simp only [ProbabilityMeasure.coe_mk, ν', ν]
    rw [Measure.map_map measurable_snd (by fun_prop)]
    rfl
  simp [phi, h₁.rdist_eq h₂, rho_eq_of_identDistrib h₁, rho_eq_of_identDistrib h₂]

-- Let $(X_1, X_2)$ be a $\phi$-minimizer, and $\tilde X_1, \tilde X_2$ be independent copies
-- of $X_1,X_2$ respectively.
variable {X₁ X₂ X₁' X₂' : Ω → G} (h_min : phiMinimizes X₁ X₂ η A ℙ)
  (h₁ : IdentDistrib X₁ X₁')
  (h₂ : IdentDistrib X₂ X₂')
  (h_indep : iIndepFun ![X₁, X₂, X₁', X₂'])
  (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂')

local notation3 "I₁" => I[X₁ + X₂ : X₁' + X₂ | X₁ + X₂ + X₁' + X₂']
local notation3 "I₂" => I[X₁ + X₂ : X₁ + X₁' | X₁ + X₂ + X₁' + X₂']
/-- `k := d[X₁ # X₂]`, the Ruzsa distance `rdist` between X₁ and X₂. -/
local notation3 "k" => d[X₁ # X₂]