\begin{proposition}[Minimizer close to reference variables]\label{tau-ref}\lean{multiTau_min_sum_le}\leanok  If $(X_i)_{1 \leq i \leq m}$ is a $\tau$-minimizer, then $\sum_{i=1}^m d[X_i; X^0] \leq \frac{2m}{\eta} d[X^0; X^0]$.
\end{proposition}
\begin{proof}\uses{tau-min-multi, multidist-nonneg, multidist-ruzsa-III}\leanok  By \Cref{tau-min-multi} we have
  $$ \tau[ (X_i)_{1 \leq i \leq m}] \leq \tau[ (X^0)_{1 \leq i \leq m}]$$
and hence by \Cref{tau-def-multi} and \Cref{multidist-nonneg}
$$ \eta \sum_{i=1}^m d[X_i; X^0] \leq D[(X^0)_{1 \leq i \leq m}] + m d[X^0; X^0].$$
The claim now follows from \Cref{multidist-ruzsa-III}.
\end{proof}
/-- If $(X_i)_{1 \leq i \leq m}$ is a $\tau$-minimizer, then $\sum_{i=1}^m d[X_i; X^0] \leq \frac{2m}{\eta} d[X^0; X^0]$. -/
lemma multiTau_min_sum_le {G Ω₀ : Type u} [hG: MeasureableFinGroup G] [hΩ₀: MeasureSpace Ω₀] (p : multiRefPackage G Ω₀) (Ω : Fin p.m → Type u) (hΩ : ∀ i, MeasureSpace (Ω i)) (hprobΩ : ∀ i, IsProbabilityMeasure (ℙ : Measure (Ω i))) (X : ∀ i, Ω i → G) (hX : ∀ i, Measurable (X i)) (h_min : multiTauMinimizes p Ω hΩ X):
  ∑ i, d[X i # p.X₀] ≤ 2 * p.m * p.η⁻¹ * d[p.X₀ # p.X₀] := by
  have hη : p.η > 0 := p.hη
  have hm : p.m > 0 := by linarith [p.hm]
  have hprob := p.hprob
  calc
    _ = p.η⁻¹ * (0 + p.η * ∑ i, d[X i # p.X₀]) := by
      field_simp
    _ ≤ p.η⁻¹ * (D[X ; hΩ] + p.η * ∑ i, d[X i # p.X₀]) := by
      gcongr
      exact multiDist_nonneg hΩ hprobΩ X hX
    _ ≤ p.η⁻¹ * (D[fun _ ↦ p.X₀ ; fun _ ↦ hΩ₀] + p.η * (p.m * d[p.X₀ # p.X₀])) := by
      apply mul_le_mul_of_nonneg_left
      · have ineq := h_min (fun _ ↦ Ω₀) (fun _ ↦ hΩ₀) (fun _ ↦ p.X₀)
        simp [multiTau] at ineq
        exact ineq
      exact inv_nonneg_of_nonneg (le_of_lt hη)
    _ ≤ p.η⁻¹ * (p.m * d[p.X₀ # p.X₀] + 1 * (p.m * d[p.X₀ # p.X₀])) := by
      gcongr
      · have : NeZero p.m := ⟨hm.ne'⟩
        apply multidist_ruzsa_III p.hm (fun _ ↦ hΩ₀) (fun _ ↦ p.X₀) _ 0
        intro _ _
        simp
        exact ProbabilityTheory.IdentDistrib.refl ( Measurable.aemeasurable p.hmeas)
      · have : 0 ≤ d[p.X₀ # p.X₀] := rdist_nonneg p.hmeas p.hmeas
        positivity
      exact p.hη'
    _ = _ := by
      field_simp
      ring


/-- If $(X_i)_{1 \leq i \leq m}$ is a $\tau$-minimizer, and $k := D[(X_i)_{1 \leq i \leq m}]$, then for any other tuple $(X'_i)_{1 \leq i \leq m}$, one has
  $$ k - D[(X'_i)_{1 \leq i \leq m}] \leq \eta \sum_{i=1}^m d[X_i; X'_i].$$
-/