tendsto_KLDiv_id_right

lemma tendsto_KLDiv_id_right [TopologicalSpace G] [DiscreteTopology G] [Finite G]    [DiscreteMeasurableSpace G] [IsFiniteMeasure μ]    {α : Type*} {l : Filter α} {ν : α → ProbabilityMeasure G} {ν' : ProbabilityMeasure G}    (h : Tendsto ν l (𝓝 ν')) (habs : ∀ x, ν' {x} = 0 → μ.map X {x} = 0) :    Tendsto (fun n ↦ KL[X ; μ # id ; ν n]) l (𝓝 (KL[X ; μ # id ; ν'])) := by  cases nonempty_fintype G  simp_rw [KLDiv_eq_sum]  apply tendsto_finsetSum _ (fun g hg ↦ ?_)  rcases eq_or_ne ((Measure.map X μ).real {g}) 0 with h'g | h'g  · simpa [h'g] using tendsto_const_nhds  apply Tendsto.mul tendsto_const_nhds  have νg : (ν' : Measure G).real {g} ≠ 0 := by    intro h    rw [measureReal_eq_zero_iff] at h    apply h'g    rw [measureReal_eq_zero_iff]    apply habs    exact (ν'.null_iff_toMeasure_null {g}).mpr h  apply Tendsto.log; swap  · simp only [Measure.map_id, ne_eq, div_eq_zero_iff, h'g, false_or, νg, not_false_eq_true]  apply Tendsto.div tendsto_const_nhds _ (by simpa using νg)  simp only [Measure.map_id]  simp only [measureReal_def]  rw [ENNReal.tendsto_toReal_iff (by simp) (by simp)]  exact (ProbabilityMeasure.tendsto_iff_forall_apply_tendsto_ennreal _ _).1 h g