Bounded convergence theorem

TheoremBounded convergence theorem, \(L^1\) form#✓fully proved

Let \(\mu\) be a finite measure on a measurable space \(\alpha\), let \(G\) be a real normed space, let \(C\) be a real number, and let \(F_n : \alpha \to G\) for \(n \in \mathbb{N}\) and \(f : \alpha \to G\) be functions. Suppose that each \(F_n\) is almost everywhere strongly measurable, that for every \(n\) we have \(\|F_n(a)\| \le C\) for \(\mu\)-almost every \(a\), and that \(F_n \to f\) in \(\mu\)-measure. Then \(\int_\alpha \|F_n(a) - f(a)\| \, d\mu(a) \to 0\) as \(n \to \infty\).

theorem tendsto_integral_norm_sub_of_bounded_convergence
    {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ]
    {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
    {F : ℕ → α → G} {f : α → G} {C : ℝ}
    (hF_meas : ∀ n, AEStronglyMeasurable (F n) μ)
    (h_bound : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ C)
    (h_lim : TendstoInMeasure μ F atTop f) :
    Tendsto (fun n ↦ ∫ a, ‖F n a - f a‖ ∂μ) atTop (𝓝 0)

TheoremBounded convergence theorem#✓fully proved

Let \(\mu\) be a finite measure on a measurable space \(\alpha\), let \(G\) be a real normed space, let \(C\) be a real number, and let \(F_n : \alpha \to G\) for \(n \in \mathbb{N}\) and \(f : \alpha \to G\) be functions. Suppose that each \(F_n\) is almost everywhere strongly measurable, that for every \(n\) we have \(\|F_n(a)\| \le C\) for \(\mu\)-almost every \(a\), and that \(F_n \to f\) in \(\mu\)-measure (in probability). Then \(\int_\alpha F_n \, d\mu \to \int_\alpha f \, d\mu\) as \(n \to \infty\).

theorem tendsto_integral_of_bounded_convergence
    {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ]
    {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
    {F : ℕ → α → G} {f : α → G} {C : ℝ}
    (hF_meas : ∀ n, AEStronglyMeasurable (F n) μ)
    (h_bound : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ C)
    (h_lim : TendstoInMeasure μ F atTop f) :
    Tendsto (fun n ↦ ∫ a, F n a ∂μ) atTop (𝓝 (∫ a, f a ∂μ))

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.