Ω : Type u_2
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.147040
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => mass (μs i)) F (𝓝 0)
⊢ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => testAgainstNN (μs i) f) F (𝓝 (testAgainstNN 0 f))
Ω : Type u_2
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.147040
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => mass (μs i)) F (𝓝 0)
⊢ Tendsto μs F (𝓝 0)
rw [tendsto_iff_forall_testAgainstNN_tendsto]
Ω : Type u_2
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.147040
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => mass (μs i)) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun i => testAgainstNN (μs i) f) F (𝓝 (testAgainstNN 0 f))
Ω : Type u_2
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.147040
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => mass (μs i)) F (𝓝 0)
⊢ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => testAgainstNN (μs i) f) F (𝓝 (testAgainstNN 0 f))
intro f
case h.e'_5.h.e'_3
Ω : Type u_2
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.147040
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => mass (μs i)) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ testAgainstNN 0 f = 0
Ω : Type u_2
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.147040
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => mass (μs i)) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun i => testAgainstNN (μs i) f) F (𝓝 (testAgainstNN 0 f))
convert tendsto_zero_testAgainstNN_of_tendsto_zero_mass mass_lim f
no goals
case h.e'_5.h.e'_3
Ω : Type u_2
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.147040
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => mass (μs i)) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ testAgainstNN 0 f = 0
rw [zero_testAgainstNN_apply]