multiTau_min_sum_le

lemma multiTau_min_sum_le {G Ω₀ : Type u} [hG : MeasurableFinGroup 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 simp; 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 _ ↦ hprob) (fun _ ↦ p.X₀)          (fun _ ↦ p.hmeas)        simp only [multiTau, Finset.sum_const, Finset.card_univ, Fintype.card_fin,          nsmul_eq_mul] 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₀) _ (fun _ ↦ p.hmeas)          (fun _ ↦ p.hprob) _ 0        · intro _ _          simpa using .refl p.hmeas.aemeasurable        intro _; infer_instance      · have : 0 ≤ d[p.X₀ # p.X₀] := rdist_nonneg p.hmeas p.hmeas        positivity      exact p.hη'    _ = _ := by      field_simp      ring