dist_of_X_U_H_le

lemma dist_of_X_U_H_le {G : Type u} [AddCommGroup G] [Finite G] [MeasurableSpace G]    [MeasurableSingletonClass G] {m : ℕ} (hm : m ≥ 2) (htorsion : ∀ x:G, m • x = 0) {Ω : Type u}    [MeasureSpace Ω] [IsProbabilityMeasure (ℙ:Measure Ω)] {X: Ω → G} (hX: Measurable X) :    ∃ H : AddSubgroup G, ∃ Ω' : Type u, ∃ mΩ : MeasureSpace Ω', IsProbabilityMeasure mΩ.volume ∧      ∃ U : Ω' → G, IsUniform H U ∧ Measurable U ∧ d[X # U] ≤ 64 * m^3 * d[X # X] := by  cases nonempty_fintype G  let _ : MeasurableFinGroup G := {  }  let p : multiRefPackage G Ω := {    m := m    hm := hm    htorsion := htorsion    hprob := inferInstance    X₀ := X    hmeas := hX    η := 1 / (32 * m^3)    hη := by positivity    hη' := by      rw [one_div, inv_le_one₀ (by positivity)]; norm_cast; linarith [Nat.pow_le_pow_left hm 3]  }  obtain ⟨Ω', mΩ', X', hX'_mes, hΩ'_prob, htau_min⟩ := multiTau_min_exists p  have hdist : D[X'; mΩ'] = 0 := by    let X'' : (q: Fin p.m × Fin p.m) → Ω' q.1 → G := fun q ω ↦ X' q.1 ω    have := independent_copies'_finiteRange X'' (by fun_prop) (fun q ↦ (mΩ' q.1).volume)    obtain ⟨Ω'', hΩ'', μ'', Y, hY_prob, hY_indep, hYi⟩ := this    let _ : MeasureSpace Ω'' := ⟨μ''⟩    have hY_mes : ∀ i, Measurable (Y i) := by intro i; specialize hYi i; tauto    have hY_ident : ∀ i, IdentDistrib (Y i) (X'' i) μ'' ℙ := by intro i; specialize hYi i; tauto    convert k_eq_zero mΩ' htau_min hΩ'_prob hX'_mes (by fun_prop) hY_indep _ (by rfl)    intro i j; specialize hY_ident (i,j); simpa  have hclose : ∃ i, d[X' i # p.X₀] ≤ (2/p.η) * d[p.X₀ # p.X₀] := by    by_contra!    replace : ∑ i:Fin p.m, 2 / p.η * d[p.X₀ # p.X₀] < ∑ i, d[X' i # p.X₀] := by      apply Finset.sum_lt_sum_of_nonempty      · use ⟨0, by linarith⟩; simp      simp [this]    simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] at this    have h' := multiTau_min_sum_le p _ mΩ' hΩ'_prob _ hX'_mes htau_min    have h'' : ↑p.m * (2 / p.η * d[p.X₀ # p.X₀]) =  2 * ↑p.m * p.η⁻¹ * d[p.X₀ # p.X₀] := by      field_simp    order  obtain ⟨i, hclose⟩ := hclose  obtain ⟨H, U, hU_mes, hU_unif, hdist⟩ :=    multidist_eq_zero hm mΩ' hΩ'_prob _ hdist hX'_mes (inferInstance) i  replace hclose : d[p.X₀ # U] ≤ (2/p.η) * d[p.X₀ # p.X₀] := calc    _ ≤ d[p.X₀ # X' i] + d[X' i # U] := rdist_triangle hX (by fun_prop) (by fun_prop)    _ = d[X' i # p.X₀] := by simpa [hdist] using rdist_symm    _ ≤ _ := hclose  refine ⟨H, Ω' i, mΩ' i, hΩ'_prob i, U, hU_unif, hU_mes, ?_⟩  convert hclose using 2  simp [p]; field_simp; ring