Prove2Me

Dominated convergence for the upper-boundary integrand

Proved
WeightedRootIntegralIdentity.upper_boundary_dominated_convergence

by abcdefg · Sep 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysisdominated-convergenceupper-boundary

Retired superseded version; use WeightedRootIntegralIdentity.upper_boundary_dominated_convergence_v4 instead.

Retired as a superseded variant; the newer proved version is retained in the WeightedRootIntegralIdentity development.

Preamble
import Mathlib
open MeasureTheory Filter
open scoped Topology
Formal statement
namespace WeightedRootIntegralIdentity
open MeasureTheory Filter
open scoped Topology

theorem upper_boundary_dominated_convergence {f : ℕ → ℝ → ℂ} {f₀ G : ℝ → ℂ} {μ : Measure ℝ}
    (hG : Integrable G μ)
    (hmeas : ∀ n, AEStronglyMeasurable (f n) μ)
    (hdom : ∀ n, ∀ᵐ x ∂μ, ‖f n x‖ ≤ ‖G x‖)
    (hlim : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f₀ x))) :
    Tendsto (fun n => ∫ x, f n x ∂μ) atTop (𝓝 (∫ x, f₀ x ∂μ)) := by sorry

end WeightedRootIntegralIdentity
Source
The Bochner dominated-convergence theorem applied to the complex-valued upper-boundary integrands.

View graph