Ω : 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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
⊢ Tendsto (fun i => testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs 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
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun i => testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f) F
    (𝓝 (testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize μ)) f))
have lim_mass := μs_lim.mass
Ω : 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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
⊢ Tendsto (fun i => testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs 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
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
⊢ Tendsto (fun i => testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f) F
    (𝓝 (testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize μ)) f))
have aux : {(0 : ℝ≥0)}ᶜ ∈ 𝓝 μ.mass :=
  isOpen_compl_singleton.mem_nhds (μ.mass_nonzero_iff.mpr nonzero)
Ω : 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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
⊢ Tendsto (fun i => testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs 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
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
⊢ Tendsto (fun i => testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f) F
    (𝓝 (testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize μ)) f))
have eventually_nonzero : ∀ᶠ i in F, μs i ≠ 0 := by
  simp_rw [← mass_nonzero_iff]
  exact lim_mass aux
Ω : 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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve :
  ∀ᶠ (i : γ) in F,
    testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f = (mass (μs i))⁻¹ * testAgainstNN (μs i) f
⊢ Tendsto (fun i => testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs 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
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
⊢ Tendsto (fun i => testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f) F
    (𝓝 (testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize μ)) f))
have eve : ∀ᶠ i in F,
    (μs i).normalize.toFiniteMeasure.testAgainstNN f =
      (μs i).mass⁻¹ * (μs i).testAgainstNN f := by
  filter_upwards [eventually_iff.mp eventually_nonzero]
  intro i hi
  apply normalize_testAgainstNN _ hi
Ω : 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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve :
  ∀ᶠ (i : γ) in F,
    testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f = (mass (μs i))⁻¹ * testAgainstNN (μs i) f
⊢ Tendsto (fun x => (mass (μs x))⁻¹ * testAgainstNN (μs x) f) F (𝓝 ((mass μ)⁻¹ * testAgainstNN μ 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
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve :
  ∀ᶠ (i : γ) in F,
    testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f = (mass (μs i))⁻¹ * testAgainstNN (μs i) f
⊢ Tendsto (fun i => testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f) F
    (𝓝 (testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize μ)) f))
simp_rw [tendsto_congr' eve, μ.normalize_testAgainstNN nonzero]
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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve :
  ∀ᶠ (i : γ) in F,
    testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f = (mass (μs i))⁻¹ * testAgainstNN (μs i) f
lim_pair : Tendsto (fun i => ((mass (μs i))⁻¹, testAgainstNN (μs i) f)) F (𝓝 ((mass μ)⁻¹, testAgainstNN μ f))
⊢ Tendsto (fun x => (mass (μs x))⁻¹ * testAgainstNN (μs x) f) F (𝓝 ((mass μ)⁻¹ * testAgainstNN μ f))
exact tendsto_mul.comp lim_pair
Ω : 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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
⊢ ∀ᶠ (i : γ) in F, mass (μs i) ≠ 0
Ω : 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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
⊢ ∀ᶠ (i : γ) in F, μs i ≠ 0
simp_rw [← mass_nonzero_iff]
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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
⊢ ∀ᶠ (i : γ) in F, mass (μs i) ≠ 0
exact lim_mass aux
case h
Ω : 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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
⊢ ∀ (a : γ),
    μs a ≠ 0 →
      testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs a))) f = (mass (μs a))⁻¹ * testAgainstNN (μs a) 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
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
⊢ ∀ᶠ (i : γ) in F,
    testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f = (mass (μs i))⁻¹ * testAgainstNN (μs i) f
filter_upwards [eventually_iff.mp eventually_nonzero]
case h
Ω : 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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
i : γ
hi : μs i ≠ 0
⊢ testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f = (mass (μs i))⁻¹ * testAgainstNN (μs i) f
case h
Ω : 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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
⊢ ∀ (a : γ),
    μs a ≠ 0 →
      testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs a))) f = (mass (μs a))⁻¹ * testAgainstNN (μs a) f
intro i hi
no goals
case h
Ω : 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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
i : γ
hi : μs i ≠ 0
⊢ testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f = (mass (μs i))⁻¹ * testAgainstNN (μs i) f
apply normalize_testAgainstNN _ hi
case refine'_1
Ω : 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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve :
  ∀ᶠ (i : γ) in F,
    testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f = (mass (μs i))⁻¹ * testAgainstNN (μs i) f
⊢ Tendsto (fun n => ((mass (μs n))⁻¹, testAgainstNN (μs n) f).fst) F (𝓝 ((mass μ)⁻¹, testAgainstNN μ f).fst)

case refine'_2
Ω : 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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve :
  ∀ᶠ (i : γ) in F,
    testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f = (mass (μs i))⁻¹ * testAgainstNN (μs i) f
⊢ Tendsto (fun n => ((mass (μs n))⁻¹, testAgainstNN (μs n) f).snd) F (𝓝 ((mass μ)⁻¹, testAgainstNN μ f).snd)
Ω : 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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve :
  ∀ᶠ (i : γ) in F,
    testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f = (mass (μs i))⁻¹ * testAgainstNN (μs i) f
⊢ Tendsto (fun i => ((mass (μs i))⁻¹, testAgainstNN (μs i) f)) F (𝓝 ((mass μ)⁻¹, testAgainstNN μ f))
refine' (Prod.tendsto_iff _ _).mpr ⟨_, _⟩
no goals
case refine'_1
Ω : 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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve :
  ∀ᶠ (i : γ) in F,
    testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f = (mass (μs i))⁻¹ * testAgainstNN (μs i) f
⊢ Tendsto (fun n => ((mass (μs n))⁻¹, testAgainstNN (μs n) f).fst) F (𝓝 ((mass μ)⁻¹, testAgainstNN μ f).fst)
exact (continuousOn_inv₀.continuousAt aux).tendsto.comp lim_mass
no goals
case refine'_2
Ω : 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
lim_mass : Tendsto (fun i => mass (μs i)) F (𝓝 (mass μ))
aux : {0}ᶜ ∈ 𝓝 (mass μ)
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve :
  ∀ᶠ (i : γ) in F,
    testAgainstNN (ProbabilityMeasure.toFiniteMeasure (normalize (μs i))) f = (mass (μs i))⁻¹ * testAgainstNN (μs i) f
⊢ Tendsto (fun n => ((mass (μs n))⁻¹, testAgainstNN (μs n) f).snd) F (𝓝 ((mass μ)⁻¹, testAgainstNN μ f).snd)
exact tendsto_iff_forall_testAgainstNN_tendsto.mp μs_lim f