Ω : Type u_2
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
⊢ ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun i => testAgainstNN ((ProbabilityMeasure.toFiniteMeasure ∘ fun i => normalize (μs i)) i) f) F
      (𝓝 (testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize μ)) f))
Ω : Type u_2
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
⊢ Tendsto (fun i => normalize (μs i)) F (𝓝 (normalize μ))
rw [ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds,
  tendsto_iff_forall_testAgainstNN_tendsto]
no goals
Ω : Type u_2
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
⊢ ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun i => testAgainstNN ((ProbabilityMeasure.toFiniteMeasure ∘ fun i => normalize (μs i)) i) f) F
      (𝓝 (testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize μ)) f))
exact fun f => tendsto_normalize_testAgainstNN_of_tendsto μs_lim nonzero f