Theorems · Theorem · measure theory

intervalIntegral.continuousWithinAt_primitive

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b₀ b₁ b₂ : ℝ} {μ : MeasureTheory.Measure ℝ}
  {f : ℝ → E},
  μ {b₀} = 0 →
    IntervalIntegrable f μ (min a b₁) (max a b₂) →
      ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Set.Icc b₁ b₂) b₀

Defined in

Mathlib.MeasureTheory.Integral.DominatedConvergence

Cited by

6 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace