Theorems · Theorem · measure theory

continuousOn_integral_bilinear_of_locally_integrable_of_compact_support

∀ {Y : Type u_2} {E : Type u_3} {F : Type u_4} {X : Type u_5} {G : Type u_6} {𝕜 : Type u_7} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure Y}
  [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedAddCommGroup E] [inst_6 : NormedSpace ℝ E]
  [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedAddCommGroup G] [inst_10 : NormedSpace 𝕜 G]
  [inst_11 : NormedSpace 𝕜 E] (L : F →L[𝕜] G →L[𝕜] E) {f : X → Y → G} {s : Set X} {k : Set Y} {g : Y → F},
  IsCompact k →
    ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ) →
      (∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0) →
        MeasureTheory.IntegrableOn g k μ → ContinuousOn (fun x => ∫ (y : Y), (L (g y)) (f x y) ∂μ) s

Consider a parameterized integral x ↦ ∫ y, L (g y) (f x y) where L is bilinear, g is locally integrable and 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 260 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceMeasurableSpaceOpensMeasurableSpaceNontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedSpace