Integration and convergence

The Lebesgue integral and its convergence theorems, modes of convergence of measurable functions, approximation by simple functions, product measures, convolution, differentiation under the integral sign and integral inequalities.

• Almost everywhere convergence
• Approximation by simple functions
• Bounded convergence theorem
• Convergence in measure
• Convolution
• Differentiation under the integral sign
• Jensen's inequality for integrals
• Products of measures with densities
• Scheffé's lemma

TheoremEgorov's theorem on the real line under integrable domination#●ready to prove

Let \(f : \mathbb{R} \to \mathbb{R}\) be any function and let \(f_n : \mathbb{R} \to \mathbb{R}\), \(n \in \mathbb{N}\), be Borel measurable functions with \(f_n(x) \to f(x)\) for almost every \(x \in \mathbb{R}\). Let \(g : \mathbb{R} \to \mathbb{R}\) be Lebesgue integrable with \(|f_n(x)| \le g(x)\) for all \(n\) and all \(x \in \mathbb{R}\). Then for every \(\varepsilon > 0\) there is a Borel set \(E \subseteq \mathbb{R}\) of Lebesgue measure less than \(\varepsilon\) such that \(f_n \to f\) uniformly on \(\mathbb{R} \setminus E\).

public theorem_wanted exists_measure_lt_tendstoUniformlyOn_compl_of_ae_tendsto_of_abs_le
  (f : ℝ → ℝ) (fn : ℕ → ℝ → ℝ) (g : ℝ → ℝ) (hfn_meas : ∀ n : ℕ, Measurable (fn n))
  (hae : ∀ᵐ x ∂MeasureTheory.volume, Filter.Tendsto (fun n : ℕ => fn n x) Filter.atTop (nhds (f x)))
  (hg : MeasureTheory.Integrable g)
  (hdom : ∀ n : ℕ, ∀ x : ℝ, |fn n x| ≤ g x) :
  ∀ ε : ℝ, ε > 0 → ∃ E : Set ℝ,
    MeasurableSet E ∧ MeasureTheory.volume E < ENNReal.ofReal ε ∧
      TendstoUniformlyOn fn f Filter.atTop Eᶜ

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Measure and integration; Classical measure theory), problem ma_proofbench_l2_43.

TheoremLusin's theorem#✓fully proved

Let \(X\) be a locally compact Hausdorff topological space with its Borel \(\sigma\)-algebra, and let \(\mu\) be a finite measure on \(X\) that is regular: finite on compact sets, outer regular, and inner regular on open sets by compact sets. Let \(Y\) be a second-countable topological space with its Borel \(\sigma\)-algebra, and let \(f : X \to Y\) be measurable. Then for every real \(\varepsilon > 0\) there is a compact set \(K \subseteq X\) with \(\mu(X \setminus K) < \varepsilon\) such that \(f\) is continuous on \(K\).

theorem lusin {α β : Type*} [TopologicalSpace α] [MeasurableSpace α]
    [BorelSpace α] [T2Space α] [LocallyCompactSpace α] [TopologicalSpace β]
    [MeasurableSpace β] [BorelSpace β] [SecondCountableTopology β] {μ : Measure α}
    [IsFiniteMeasure μ] [Regular μ] {f : α → β} (hf : Measurable f) {ε : ℝ}
    (hε : 0 < ε) :
    ∃ K : Set α, IsCompact K ∧ μ (Kᶜ) < ENNReal.ofReal ε ∧ ContinuousOn f K

Sources

• G. B. Folland, Real Analysis, 2nd ed., Lusin's theorem.

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.