English
Under suitable hypotheses, the map x ↦ ∫_Y L(g(y), f(x,y)) dμ(y) is continuous on s, when f is locally integrable and has compact support with respect to y, and L is bilinear.
Русский
При заданных условиях отображение x ↦ ∫_Y L(g(y), f(x,y)) dμ(y) непрерывно на s, если f по y локально интегрируема и имеет компактную опору, а L линейно-билинейна.
LaTeX
$$$$\\text{continuousOn } s \\ mapsto \\int_Y L(g(y), f(x,y)) dμ(y)$$$$
Lean4
/-- Consider a parameterized integral `x ↦ ∫ y, f x y` where `f` is continuous and uniformly
compactly supported. Then the integral depends continuously on `x`. -/
theorem continuousOn_integral_of_compact_support {f : X → Y → E} {s : Set X} {k : Set Y} [IsFiniteMeasureOnCompacts μ]
(hk : IsCompact k) (hf : ContinuousOn f.uncurry (s ×ˢ univ)) (hfs : ∀ p, ∀ x, p ∈ s → x ∉ k → f p x = 0) :
ContinuousOn (fun x ↦ ∫ y, f x y ∂μ) s := by
simpa using
continuousOn_integral_bilinear_of_locally_integrable_of_compact_support (lsmul ℝ ℝ) hk hf hfs
(integrableOn_const hk.measure_ne_top) (g := fun _ ↦ 1)
