\begin{theorem}[Limiting improved $\tau$-decrement]\label{de-prop-lim-improv}\lean{tau_minimizer_exists_rdist_eq_zero}\leanok
For $\eta = 1/8$, there exist tau-minimizers $X_1, X_2$ satisfying $d[X_1;X_2] = 0$.
\end{theorem}
\begin{proof}\uses{de-prop-improv, tau-min}\leanok
For each $\eta<1/8$, consider minimizers $X_1^\eta$ and $X_2^\eta$ from \Cref{tau-min}.
By \Cref{de-prop-improv},
they satisfy $d[X_1^\eta; X_2^\eta]=0$. By compactness of the space of probability measures
on $G$, one may extract a converging subsequence of the distributions of $X_1^\eta$ and $X_2^\eta$
as $\eta \to 1/8$. By continuity of all the involved quantities, the limit is a pair of
tau-minimizers for $1/8$ satisfying additionally $d[X_1;X_2] = 0$.
\end{proof}
lemma tau_minimizer_exists_rdist_eq_zero :
    ∃ (Ω : Type uG) (_ : MeasureSpace Ω) (X₁ : Ω → G) (X₂ : Ω → G),
      Measurable X₁ ∧ Measurable X₂ ∧ IsProbabilityMeasure (ℙ : Measure Ω) ∧ tau_minimizes p X₁ X₂
      ∧ d[X₁ # X₂] = 0 := by
  -- let `uₙ` be a sequence converging from below to `η`. In particular, `uₙ < 1/8`.
  obtain ⟨u, -, u_mem, u_lim⟩ :
      ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Set.Ioo 0 p.η) ∧ Tendsto u atTop (𝓝 p.η) :=
    exists_seq_strictMono_tendsto' p.hη
  -- For each `n`, consider a minimizer associated to `η = uₙ`.
  let q : ℕ → refPackage Ω₀₁ Ω₀₂ G := fun n ↦
    ⟨p.X₀₁, p.X₀₂, p.hmeas1, p.hmeas2, u n, (u_mem n).1, by linarith [(u_mem n).2, p.hη']⟩
  have : ∀ n, ∃ (μ : Measure G × Measure G),
    IsProbabilityMeasure μ.1 ∧ IsProbabilityMeasure μ.2 ∧
      ∀ (ν₁ : Measure G) (ν₂ : Measure G), IsProbabilityMeasure ν₁ → IsProbabilityMeasure ν₂ →
      τ[id ; μ.1 # id ; μ.2 | q n] ≤ τ[id ; ν₁ # id ; ν₂ | q n] :=
    fun n ↦ tau_min_exists_measure (q n)
  choose μ μ1_prob μ2_prob hμ using this
  -- The minimizer associated to `uₙ` is at zero Rusza distance of itself, by
  -- lemma `tau_strictly_decreases'`.
  have I n : d[id ; (μ n).1 # id ; (μ n).2] = 0 := by
    let M : MeasureSpace (G × G) := ⟨(μ n).1.prod (μ n).2⟩
    have : IsProbabilityMeasure ((μ n).1.prod (μ n).2) := by infer_instance
    have : d[@Prod.fst G G # @Prod.snd G G] = d[id ; (μ n).1 # id ; (μ n).2] :=
      IdentDistrib.rdist_eq IdentDistrib.fst_id IdentDistrib.snd_id
    rw [← this]
    apply tau_strictly_decreases' (q n) measurable_fst measurable_snd ?_
      (by linarith [(u_mem n).2, p.hη'])
    intro ν₁ ν₂ h₁ h₂
    have A : τ[@Prod.fst G G # @Prod.snd G G | q n] = τ[id ; (μ n).1 # id ; (μ n).2 | q n] :=
      ProbabilityTheory.IdentDistrib.tau_eq (q n) IdentDistrib.fst_id IdentDistrib.snd_id
    rw [A]
    exact hμ n _ _ h₁ h₂
  -- extract a converging subsequence of the sequence of minimizers, seen as pairs of probability
  -- measures on `G` (which is a compact space).
  let μ' : ℕ → ProbabilityMeasure G × ProbabilityMeasure G :=
    fun n ↦ (⟨(μ n).1, μ1_prob n⟩, ⟨(μ n).2, μ2_prob n⟩)
  let _i : TopologicalSpace G := (⊥ : TopologicalSpace G)
  have : DiscreteTopology G := ⟨rfl⟩
  -- The limiting pair of measures will be the desired minimizer.
  rcases IsCompact.tendsto_subseq (x := μ') isCompact_univ (fun n ↦ mem_univ _)
    with ⟨ν, -, φ, φmono, hν⟩
  have φlim : Tendsto φ atTop atTop := φmono.tendsto_atTop
  let M : MeasureSpace (G × G) := ⟨(ν.1 : Measure G).prod ν.2⟩
  have P : IsProbabilityMeasure ((ν.1 : Measure G).prod (ν.2 : Measure G)) := by infer_instance
  refine ⟨G × G, M, Prod.fst, Prod.snd, measurable_fst, measurable_snd, P, ?_, ?_⟩
  -- check that it is indeed a minimizer, as a limit of minimizers.
  · intro ν₁ ν₂ h₁ h₂
    have A : τ[@Prod.fst G G # @Prod.snd G G | p] = τ[id ; ν.1 # id ; ν.2 | p] :=
      ProbabilityTheory.IdentDistrib.tau_eq p IdentDistrib.fst_id IdentDistrib.snd_id
    rw [A]
    have L1 : Tendsto (fun n ↦ τ[id ; (μ (φ n)).1 # id ; (μ (φ n)).2 | q (φ n)]) atTop
        (𝓝 (τ[id ; ν.1 # id ; ν.2 | p])) := by
      apply Tendsto.add (Tendsto.add ?_ (Tendsto.mul (u_lim.comp φlim) ?_))
          (Tendsto.mul (u_lim.comp φlim) ?_)
      · apply Tendsto.comp (continuous_rdist_restrict_probabilityMeasure.tendsto _) hν
      · have : Continuous
          (fun (μ : ProbabilityMeasure G × ProbabilityMeasure G) ↦ d[p.X₀₁ ; ℙ # id ; μ.1]) :=
        Continuous.comp (continuous_rdist_restrict_probabilityMeasure₁' _ _ p.hmeas1) continuous_fst
        apply Tendsto.comp (this.tendsto _) hν
      · have : Continuous
          (fun (μ : ProbabilityMeasure G × ProbabilityMeasure G) ↦ d[p.X₀₂ ; ℙ # id ; μ.2]) :=
        Continuous.comp (continuous_rdist_restrict_probabilityMeasure₁' _ _ p.hmeas2) continuous_snd
        apply Tendsto.comp (this.tendsto _) hν
    have L2 : Tendsto (fun n ↦ τ[id ; ν₁ # id ; ν₂ | q (φ n)]) atTop
        (𝓝 (τ[id ; ν₁ # id ; ν₂ | p])) :=
      Tendsto.add (Tendsto.add tendsto_const_nhds (Tendsto.mul (u_lim.comp φlim)
        tendsto_const_nhds)) (Tendsto.mul (u_lim.comp φlim) tendsto_const_nhds)
    exact le_of_tendsto_of_tendsto' L1 L2 (fun n ↦ hμ (φ n) _ _ h₁ h₂)
  -- check that it has zero Rusza distance, as a limit of a sequence at zero Rusza distance.
  · have : d[@Prod.fst G G # @Prod.snd G G] = d[id ; ν.1 # id ; ν.2] :=
      IdentDistrib.rdist_eq IdentDistrib.fst_id IdentDistrib.snd_id
    rw [this]
    have L1 : Tendsto (fun n ↦ d[id ; (μ (φ n)).1 # id ; (μ (φ n)).2]) atTop
      (𝓝 (d[id ; ν.1 # id ; (ν.2 : Measure G)])) := by
        apply Tendsto.comp (continuous_rdist_restrict_probabilityMeasure.tendsto _) hν
    have L2 : Tendsto (fun n ↦ d[id ; (μ (φ n)).1 # id ; (μ (φ n)).2]) atTop (𝓝 0) := by simp [I]
    exact tendsto_nhds_unique L1 L2

/-- `entropic_PFR_conjecture_improv`: For two $G$-valued random variables $X^0_1, X^0_2$, there is some
    subgroup $H \leq G$ such that $d[X^0_1;U_H] + d[X^0_2;U_H] \le 10 d[X^0_1;X^0_2]$. -/