Theorems · Theorem · measure theory

continuousOn_integral_of_compact_support

∀ {Y : Type u_2} {E : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure Y} [inst_4 : NormedAddCommGroup E]
  [inst_5 : NormedSpace ℝ E] {f : X → Y → E} {s : Set X} {k : Set Y} [MeasureTheory.IsFiniteMeasureOnCompacts μ],
  IsCompact k →
    ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ) →
      (∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0) → ContinuousOn (fun x => ∫ (y : Y), f x y ∂μ) s

Consider a parameterized integral x ↦ ∫ y, f x y where f is continuous and uniformly compactly supported. Then the integral depends continuously on x.

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Set

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceMeasurableSpaceOpensMeasurableSpaceNormedAddCommGroupNormedSpaceMeasureTheory.IsFiniteMeasureOnCompacts