tendsto_iff_forall_integral_rclike_tendsto

English

The same convergence principle as above holds for测试 functions valued in a real/complex-like field 𝕜 (RCLike).

Русский

Та же принцип сходжения применим к тест-функциям, стоящим в поле 𝕜, подобном вещественным или комплексным.

LaTeX

$$$Tendsto(μ_s, F, 𝓝(μ)) \\iff \\forall f ∈ C_b(Ω, 𝕜),\\ Tendsto\\big(i \\mapsto \\int f \\; d(μ_s i)\\big) F (𝓝(\\int f \\; dμ))$$$

Lean4

theorem tendsto_iff_forall_integral_rclike_tendsto {γ : Type*} (𝕜 : Type*) [RCLike 𝕜] {F : Filter γ}
    {μs : γ → FiniteMeasure Ω} {μ : FiniteMeasure Ω} :
    Tendsto μs F (𝓝 μ) ↔
      ∀ f : Ω →ᵇ 𝕜, Tendsto (fun i ↦ ∫ ω, f ω ∂(μs i : Measure Ω)) F (𝓝 (∫ ω, f ω ∂(μ : Measure Ω))) :=
  by
  rw [tendsto_iff_forall_integral_tendsto]
  refine ⟨fun h f ↦ ?_, fun h f ↦ ?_⟩
  · rw [← integral_re_add_im (integrable μ f)]
    simp_rw [← integral_re_add_im (integrable (μs _) f)]
    refine Tendsto.add ?_ ?_
    · exact (RCLike.continuous_ofReal.tendsto _).comp (h (f.comp RCLike.re RCLike.lipschitzWith_re))
    ·
      exact
        (Tendsto.comp (RCLike.continuous_ofReal.tendsto _) (h (f.comp RCLike.im RCLike.lipschitzWith_im))).mul_const _
  · specialize h ((RCLike.ofRealAm (K := 𝕜)).compLeftContinuousBounded ℝ RCLike.lipschitzWith_ofReal f)
    simp only [AlgHom.compLeftContinuousBounded_apply_apply, RCLike.ofRealAm_coe, integral_ofReal] at h
    exact tendsto_ofReal_iff'.mp h

Похожие утверждения