English
For all μ and f, (μ.toWeakDualBCNN) f = μ.testAgainstNN f; i.e., evaluation aligns with integration.
Русский
Для всех μ и f выражение (μ.toWeakDualBCNN) f совпадает с μ.testAgainstNN f; т.е. обоснование совпадает с интегрированием.
LaTeX
$$$ \forall \mu : \text{FiniteMeasure } \Omega, \; \forall f : \Omega \to^{} \mathbb{R}_{\ge 0}, (\mu.toWeakDualBCNN) f = \mu.testAgainstNN f. $$$
Lean4
/-- If the total masses of finite measures tend to zero, then the measures tend to
zero. This formulation concerns the associated functionals on bounded continuous
nonnegative test functions. See `MeasureTheory.FiniteMeasure.tendsto_zero_of_tendsto_zero_mass` for
a formulation stating the weak convergence of measures. -/
theorem tendsto_zero_testAgainstNN_of_tendsto_zero_mass {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω}
(mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 0)) (f : Ω →ᵇ ℝ≥0) :
Tendsto (fun i ↦ (μs i).testAgainstNN f) F (𝓝 0) :=
by
apply tendsto_iff_dist_tendsto_zero.mpr
have obs := fun i ↦ (μs i).testAgainstNN_lipschitz_estimate f 0
simp_rw [testAgainstNN_zero, zero_add] at obs
simp_rw [show ∀ i, dist ((μs i).testAgainstNN f) 0 = (μs i).testAgainstNN f by
simp only [dist_nndist, NNReal.nndist_zero_eq_val', imp_true_iff]]
apply squeeze_zero (fun i ↦ NNReal.coe_nonneg _) obs
have lim_pair : Tendsto (fun i ↦ (⟨nndist f 0, (μs i).mass⟩ : ℝ × ℝ)) F (𝓝 ⟨nndist f 0, 0⟩) :=
(Prod.tendsto_iff _ _).mpr ⟨tendsto_const_nhds, (NNReal.continuous_coe.tendsto 0).comp mass_lim⟩
simpa using tendsto_mul.comp lim_pair
