phiMinimizer_exists_rdist_eq_zero

lemma phiMinimizer_exists_rdist_eq_zero (hA : A.Nonempty) :    ∃ (Ω : Type uG) (_ : MeasureSpace Ω) (X₁ : Ω → G) (X₂ : Ω → G),      Measurable X₁ ∧ Measurable X₂ ∧ IsProbabilityMeasure (ℙ : Measure Ω)      ∧ phiMinimizes X₁ X₂ (1/8 : ℝ) A ℙ ∧ d[X₁ # X₂] = 0 := by    -- let `uₙ` be a sequence converging from below to `η`. In particular, `uₙ < 1/8`.  obtain ⟨u, -, u_mem, u_lim⟩ :      ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Set.Ioo 0 (1/8 : ℝ)) ∧ Tendsto u atTop (𝓝 (1/8)) :=    exists_seq_strictMono_tendsto' (by norm_num)  -- For each `n`, consider a minimizer associated to `η = uₙ`.  have : ∀ n, ∃ (μ : Measure (G × G)), IsProbabilityMeasure μ ∧      phiMinimizes Prod.fst Prod.snd (u n) A μ := fun n ↦ phi_min_exists hA  choose μ μ_prob hμ using this  -- extract a converging subsequence of the sequence of minimizers, seen as pairs of probability  -- measures on `G` (which is a compact space).  let μ' : ℕ → ProbabilityMeasure (G × G) := fun n ↦ ⟨μ n, μ_prob n⟩  let _i : TopologicalSpace G := (⊥ : TopologicalSpace G)  have : DiscreteTopology G := ⟨rfl⟩  -- The limiting pair of measures will be the desired minimizer.  rcases IsCompact.tendsto_subseq (x := μ') isCompact_univ (fun n ↦ mem_univ _)    with ⟨ν, -, φ, φmono, hν⟩  have φlim : Tendsto φ atTop atTop := φmono.tendsto_atTop  let M : MeasureSpace (G × G) := ⟨ν⟩  have : IsProbabilityMeasure (ℙ : Measure (G × G)) := ν.instIsProbabilityMeasureToMeasure  refine ⟨G × G, M, Prod.fst, Prod.snd, measurable_fst, measurable_snd, by infer_instance, ?_, ?_⟩  -- check that it is indeed a minimizer, as a limit of minimizers.  · intro Ω' mΩ' X' Y' hP hX' hY'    have I n : phi Prod.fst Prod.snd (u n) A (μ n) ≤ phi X' Y' (u n) A ℙ :=      hμ n _ _ _ _ hP hX' hY'    have L1 : Tendsto (fun n ↦ phi Prod.fst Prod.snd (u (φ n)) A (μ (φ n))) atTop        (𝓝 (phi Prod.fst Prod.snd (1/8) A ν)) := by      apply Tendsto.add      · apply tendsto_rdist_probabilityMeasure continuous_fst continuous_snd hν      apply Tendsto.mul (u_lim.comp φlim)      apply Tendsto.add      · apply tendsto_rho_probabilityMeasure continuous_fst hA hν      · apply tendsto_rho_probabilityMeasure continuous_snd hA hν    have L2 : Tendsto (fun n ↦ phi X' Y' (u (φ n)) A ℙ) atTop (𝓝 (phi X' Y' (1/8) A ℙ)) :=      Tendsto.const_add _ (Tendsto.mul_const _ (u_lim.comp φlim))    exact le_of_tendsto_of_tendsto' L1 L2 (fun n ↦ I _)  -- check that it has zero Rusza distance, as a limit of a sequence at zero Rusza distance.  · -- The minimizer associated to `uₙ` is at zero Rusza distance of itself, by    -- lemma `tau_strictly_decreases'`.    have I0 n : d[Prod.fst ; μ n # Prod.snd ; μ n] = 0 := by      let M : MeasureSpace (G × G) := ⟨μ n⟩      apply dist_of_min_eq_zero (u_mem n).1 (hμ n) measurable_fst measurable_snd hA (u_mem n).2    have : Tendsto (fun x ↦ d[Prod.fst ; μ (φ x) # Prod.snd ; μ (φ x)]) atTop        (𝓝 d[@Prod.fst G G # @Prod.snd G G]) := by      apply tendsto_rdist_probabilityMeasure continuous_fst continuous_snd hν    simp_rw [I0, tendsto_const_nhds_iff] at this    exact this.symm