Theorems · Theorem · measure theory

intervalIntegral.continuousAt_parametric_primitive_of_dominated

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

Defined in

Mathlib.MeasureTheory.Integral.DominatedConvergence

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceFirstCountableTopology