exists_isUniform_of_rdist_self_eq_zero

theorem exists_isUniform_of_rdist_self_eq_zero (hX : Measurable X) (hdist : d[X # X] = 0) :    ∃ H : AddSubgroup G, ∃ U : Ω → G, Measurable U ∧ IsUniform H U ∧ d[X # U] = 0 := by  -- use for `U` a translate of `X` to make sure that `0` is in its support.  obtain ⟨x₀, h₀⟩ : ∃ x₀, ℙ (X ⁻¹' {x₀}) ≠ 0 := by    by_contra! h    have A a : (ℙ : Measure Ω).map X {a} = 0 := by      rw [Measure.map_apply hX .of_discrete]      exact h _    have B : (ℙ : Measure Ω).map X = 0 := by      rw [← Measure.sum_smul_dirac (μ := (ℙ : Measure Ω).map X)]      simp [A]    have : IsProbabilityMeasure ((ℙ : Measure Ω).map X) :=      Measure.isProbabilityMeasure_map hX.aemeasurable    exact IsProbabilityMeasure.ne_zero _ B  refine ⟨symmGroup X hX, fun ω ↦ X ω - x₀, hX.sub_const _,    isUniform_sub_const_of_rdist_eq_zero hX hdist h₀, ?_⟩  simp_rw [sub_eq_add_neg, ← Pi.add_def, rdist_add_const hX hX, hdist]