tau_minimizer_exists_rdist_eq_zero

lemma tau_minimizer_exists_rdist_eq_zero :    ∃ (Ω : Type uG) (_ : MeasureSpace Ω) (X₁ : Ω → G) (X₂ : Ω → G),      Measurable X₁ ∧ Measurable X₂ ∧ IsProbabilityMeasure (ℙ : Measure Ω) ∧ tau_minimizes p X₁ X₂      ∧ 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 p.η) ∧ Tendsto u atTop (𝓝 p.η) :=    exists_seq_strictMono_tendsto' p.hη  -- For each `n`, consider a minimizer associated to `η = uₙ`.  let q : ℕ → refPackage Ω₀₁ Ω₀₂ G := fun n ↦    ⟨p.X₀₁, p.X₀₂, p.hmeas1, p.hmeas2, u n, (u_mem n).1, by linarith [(u_mem n).2, p.hη']⟩  have : ∀ n, ∃ (μ : Measure G × Measure G),    IsProbabilityMeasure μ.1 ∧ IsProbabilityMeasure μ.2 ∧      ∀ (ν₁ : Measure G) (ν₂ : Measure G), IsProbabilityMeasure ν₁ → IsProbabilityMeasure ν₂ →      τ[id ; μ.1 # id ; μ.2 | q n] ≤ τ[id ; ν₁ # id ; ν₂ | q n] :=    fun n ↦ tau_min_exists_measure (q n)  choose μ μ1_prob μ2_prob hμ using this  -- The minimizer associated to `uₙ` is at zero Rusza distance of itself, by  -- lemma `tau_strictly_decreases'`.  have I n : d[id ; (μ n).1 # id ; (μ n).2] = 0 := by    let M : MeasureSpace (G × G) := ⟨(μ n).1.prod (μ n).2⟩    have : IsProbabilityMeasure ((μ n).1.prod (μ n).2) := by infer_instance    have : d[@Prod.fst G G # @Prod.snd G G] = d[id ; (μ n).1 # id ; (μ n).2] :=      IdentDistrib.rdist_congr IdentDistrib.fst_id IdentDistrib.snd_id    rw [← this]    apply tau_strictly_decreases' (q n) measurable_fst measurable_snd ?_      (by linarith [(u_mem n).2, p.hη'])    intro ν₁ ν₂ h₁ h₂    have A : τ[@Prod.fst G G # @Prod.snd G G | q n] = τ[id ; (μ n).1 # id ; (μ n).2 | q n] :=      ProbabilityTheory.IdentDistrib.tau_eq (q n) IdentDistrib.fst_id IdentDistrib.snd_id    rw [A]    exact hμ n _ _ h₁ h₂  -- 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 × ProbabilityMeasure G :=    fun n ↦ (⟨(μ n).1, μ1_prob n⟩, ⟨(μ n).2, μ2_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) := ⟨(ν.1 : Measure G).prod ν.2⟩  have P : IsProbabilityMeasure ((ν.1 : Measure G).prod (ν.2 : Measure G)) := by infer_instance  refine ⟨G × G, M, Prod.fst, Prod.snd, measurable_fst, measurable_snd, P, ?_, ?_⟩  -- check that it is indeed a minimizer, as a limit of minimizers.  · intro ν₁ ν₂ h₁ h₂    have A : τ[@Prod.fst G G # @Prod.snd G G | p] = τ[id ; ν.1 # id ; ν.2 | p] :=      ProbabilityTheory.IdentDistrib.tau_eq p IdentDistrib.fst_id IdentDistrib.snd_id    rw [A]    have L1 : Tendsto (fun n ↦ τ[id ; (μ (φ n)).1 # id ; (μ (φ n)).2 | q (φ n)]) atTop        (𝓝 (τ[id ; ν.1 # id ; ν.2 | p])) := by      apply Tendsto.add (Tendsto.add ?_ (Tendsto.mul (u_lim.comp φlim) ?_))          (Tendsto.mul (u_lim.comp φlim) ?_)      · apply Tendsto.comp (continuous_rdist_restrict_probabilityMeasure.tendsto _) hν      · have : Continuous          (fun (μ : ProbabilityMeasure G × ProbabilityMeasure G) ↦ d[p.X₀₁ ; ℙ # id ; μ.1]) :=        Continuous.comp (continuous_rdist_restrict_probabilityMeasure₁' _ _ p.hmeas1) continuous_fst        apply Tendsto.comp (this.tendsto _) hν      · have : Continuous          (fun (μ : ProbabilityMeasure G × ProbabilityMeasure G) ↦ d[p.X₀₂ ; ℙ # id ; μ.2]) :=        Continuous.comp (continuous_rdist_restrict_probabilityMeasure₁' _ _ p.hmeas2) continuous_snd        apply Tendsto.comp (this.tendsto _) hν    have L2 : Tendsto (fun n ↦ τ[id ; ν₁ # id ; ν₂ | q (φ n)]) atTop        (𝓝 (τ[id ; ν₁ # id ; ν₂ | p])) :=      Tendsto.add (Tendsto.add tendsto_const_nhds (Tendsto.mul (u_lim.comp φlim)        tendsto_const_nhds)) (Tendsto.mul (u_lim.comp φlim) tendsto_const_nhds)    exact le_of_tendsto_of_tendsto' L1 L2 (fun n ↦ hμ (φ n) _ _ h₁ h₂)  -- check that it has zero Rusza distance, as a limit of a sequence at zero Rusza distance.  · have : d[@Prod.fst G G # @Prod.snd G G] = d[id ; ν.1 # id ; ν.2] :=      IdentDistrib.rdist_congr IdentDistrib.fst_id IdentDistrib.snd_id    rw [this]    have L1 : Tendsto (fun n ↦ d[id ; (μ (φ n)).1 # id ; (μ (φ n)).2]) atTop      (𝓝 (d[id ; ν.1 # id ; (ν.2 : Measure G)])) := by        apply Tendsto.comp (continuous_rdist_restrict_probabilityMeasure.tendsto _) hν    have L2 : Tendsto (fun n ↦ d[id ; (μ (φ n)).1 # id ; (μ (φ n)).2]) atTop (𝓝 0) := by simp [I]    exact tendsto_nhds_unique L1 L2