Theorems · Theorem · measure theory

intervalIntegral.continuousAt_of_dominated_interval

∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {X : Type u_3}
  [inst_2 : TopologicalSpace X] [FirstCountableTopology X] {F : X → ℝ → E} {x₀ : X} {bound : ℝ → ℝ} {a b : ℝ},
  (∀ᶠ (x : X) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) →
    (∀ᶠ (x : X) in nhds x₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ‖F x t‖ ≤ bound t) →
      IntervalIntegrable bound μ a b →
        (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ContinuousAt (fun x => F x t) x₀) →
          ContinuousAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) x₀

Continuity of interval integral with respect to a parameter at a point. Given F : X → ℝ → E, assume F x is ae-measurable on [a, b] for x in a neighborhood of x₀, and assume it is bounded by a function integrable on [a, b] independent of x in a neighborhood of x₀. If (fun x ↦ F x t) is continuous at x₀ for almost every t in [a, b] then the same holds for (fun x ↦ ∫ t in a..b, F x t ∂μ) s x₀.

Defined in

Mathlib.MeasureTheory.Integral.DominatedConvergence

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceFirstCountableTopology