Theorems · Theorem · measure theory

intervalIntegral.continuousWithinAt_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 : ℝ}
  {s : Set X},
  (∀ᶠ (x : X) in nhdsWithin x₀ s, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) →
    (∀ᶠ (x : X) in nhdsWithin x₀ s, ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ‖F x t‖ ≤ bound t) →
      IntervalIntegrable bound μ a b →
        (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ContinuousWithinAt (fun x => F x t) s x₀) →
          ContinuousWithinAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) s x₀

Continuity of interval integral with respect to a parameter, at a point within a set. Given F : X → ℝ → E, assume F x is ae-measurable on [a, b] for x in a neighborhood of x₀ within s and at x₀, and assume it is bounded by a function integrable on [a, b] independent of x in a neighborhood of x₀ within s. If (fun x ↦ F x t) is continuous at x₀ within s 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

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceFirstCountableTopology