Theorems · Theorem · measure theory

intervalIntegral.hasSum_integral_of_dominated_convergence

∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ} {ι : Type u_3} [Countable ι] {F : ι → ℝ → E} (bound : ι → ℝ → ℝ),
  (∀ (n : ι), MeasureTheory.AEStronglyMeasurable (F n) (μ.restrict (Set.uIoc a b))) →
    (∀ (n : ι), ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ‖F n t‖ ≤ bound n t) →
      (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → Summable fun n => bound n t) →
        IntervalIntegrable (fun t => ∑' (n : ι), bound n t) μ a b →
          (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → HasSum (fun n => F n t) (f t)) →
            HasSum (fun n => ∫ (t : ℝ) in a..b, F n t ∂μ) (∫ (t : ℝ) in a..b, f t ∂μ)

Lebesgue dominated convergence theorem for parametric interval integrals.

Defined in

Mathlib.MeasureTheory.Integral.DominatedConvergence

Cited by

2 results in Mathlib

Foundations

Depth 256 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCountable