multidist_ruzsa_II

lemma multidist_ruzsa_II {m : ℕ} (hm : m ≥ 2) {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i))    (hprob : ∀ i, IsProbabilityMeasure (hΩ i).volume) (X : ∀ i, Ω i → G)    (hmes : ∀ i, Measurable (X i)) (hfin : ∀ i, FiniteRange (X i)) :    ∑ j, d[X j # X j] ≤ 2 * m * D[X; hΩ] := by  have claim (j k: Fin m) (hjk: j ≠ k) : d[X j # X j] ≤ 2 * d[X j # - X k] := calc    _ ≤ d[X j # - X k] + d[-X k # X j] := rdist_triangle (hmes j) (hmes k).neg (hmes j)    _ = d[X j # - X k] + d[X j # -X k] := by congr 1; apply rdist_symm    _ = 2 * d[X j # - X k] := by ring  replace claim := offDiag_sum_le _ _ claim  have hm' : m ≥ 1 := by linarith  have claim2 : offDiag_sum (fun j k ↦ d[X j # - X k]) ≤ m * (m - 1) * D[X; hΩ] :=    multidist_ruzsa_I hm' _ hmes hprob hfin  rw [offDiag_sum_left hm', offDiag_mul_sum] at claim  have : (m:ℝ) - 1 > 0 := by    have : (m:ℝ) ≥ 2 := by simp [hm]    linarith  calc    _ = (m - 1 : ℝ)⁻¹ * (m - 1) * ∑ j, d[X j # X j] := by      field_simp [this]    _ ≤ (m - 1 : ℝ)⁻¹ * 2 * offDiag_sum fun j k ↦ d[X j # -X k] := by      rw [mul_assoc, mul_assoc]      gcongr    _ ≤ (m - 1 : ℝ)⁻¹ * 2 * (m * (m - 1) * D[X ; hΩ]) := by gcongr    _ = 2 * m * D[X; hΩ] := by field_simp [this]