English
If a function f: X × Y → E is jointly continuous, then the parametric integral x ↦ ∫_Y f(x,y) dμ(y) is continuous in x, under suitable topological hypotheses on X, Y and μ.
Русский
При совместной непрерывности f: X × Y → E неперывность параметрического интеграла x ↦ ∫_Y f(x,y) dμ(y) сохраняется при подходящих условия на X, Y и μ.
LaTeX
$$$$\\text{continuous in }x \\text{ of } x \\mapsto \\int_Y f(x,y) \\,dμ(y)$$ under assumptions.$$
Lean4
/-- 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`. -/
theorem continuousOn_integral_bilinear_of_locally_integrable_of_compact_support [NormedSpace 𝕜 E]
(L : F →L[𝕜] G →L[𝕜] E) {f : X → Y → G} {s : Set X} {k : Set Y} {g : Y → F} (hk : IsCompact k)
(hf : ContinuousOn f.uncurry (s ×ˢ univ)) (hfs : ∀ p, ∀ x, p ∈ s → x ∉ k → f p x = 0) (hg : IntegrableOn g k μ) :
ContinuousOn (fun x ↦ ∫ y, L (g y) (f x y) ∂μ) s :=
by
have A : ∀ p ∈ s, Continuous (f p) := fun p hp ↦
by
refine hf.comp_continuous (.prodMk_right _) fun y => ?_
simpa only [prodMk_mem_set_prod_eq, mem_univ, and_true] using hp
intro q hq
apply Metric.continuousWithinAt_iff'.2 (fun ε εpos ↦ ?_)
obtain ⟨δ, δpos, hδ⟩ : ∃ (δ : ℝ), 0 < δ ∧ ∫ x in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε := by
simpa [integral_mul_const] using exists_pos_mul_lt εpos _
obtain ⟨v, v_mem, hv⟩ : ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ k, dist (f p x) (f q x) < δ :=
hk.mem_uniformity_of_prod (hf.mono (Set.prod_mono_right (subset_univ k))) hq (dist_mem_uniformity δpos)
simp_rw [dist_eq_norm] at hv ⊢
have I : ∀ p ∈ s, IntegrableOn (fun y ↦ L (g y) (f p y)) k μ :=
by
intro p hp
obtain ⟨C, hC⟩ : ∃ C, ∀ y, ‖f p y‖ ≤ C :=
by
have : ContinuousOn (f p) k :=
by
have : ContinuousOn (fun y ↦ (p, y)) k := by fun_prop
exact hf.comp this (by simp [MapsTo, hp])
rcases IsCompact.exists_bound_of_continuousOn hk this with ⟨C, hC⟩
refine ⟨max C 0, fun y ↦ ?_⟩
by_cases hx : y ∈ k
· exact (hC y hx).trans (le_max_left _ _)
· simp [hfs p y hp hx]
have : IntegrableOn (fun y ↦ ‖L‖ * ‖g y‖ * C) k μ := (hg.norm.const_mul _).mul_const _
apply Integrable.mono' this ?_ ?_
· borelize G
apply L.aestronglyMeasurable_comp₂ hg.aestronglyMeasurable
apply StronglyMeasurable.aestronglyMeasurable
apply Continuous.stronglyMeasurable_of_support_subset_isCompact (A p hp) hk
apply support_subset_iff'.2 (fun y hy ↦ hfs p y hp hy)
· apply Eventually.of_forall (fun y ↦ (le_opNorm₂ L (g y) (f p y)).trans ?_)
gcongr
apply hC
filter_upwards [v_mem, self_mem_nhdsWithin] with p hp h'p
calc
‖∫ x, L (g x) (f p x) ∂μ - ∫ x, L (g x) (f q x) ∂μ‖ =
‖∫ x in k, L (g x) (f p x) ∂μ - ∫ x in k, L (g x) (f q x) ∂μ‖ :=
by
congr 2
· refine (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
simp [hfs p y h'p hy]
· refine (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
simp [hfs q y hq hy]
_ = ‖∫ x in k, L (g x) (f p x) - L (g x) (f q x) ∂μ‖ := by rw [integral_sub (I p h'p) (I q hq)]
_ ≤ ∫ x in k, ‖L (g x) (f p x) - L (g x) (f q x)‖ ∂μ := (norm_integral_le_integral_norm _)
_ ≤ ∫ x in k, ‖L‖ * ‖g x‖ * δ ∂μ :=
by
apply integral_mono_of_nonneg (Eventually.of_forall (fun y ↦ by positivity))
· exact (hg.norm.const_mul _).mul_const _
· filter_upwards with y
by_cases hy : y ∈ k
· dsimp only
specialize hv p hp y hy
calc
‖L (g y) (f p y) - L (g y) (f q y)‖ = ‖L (g y) (f p y - f q y)‖ := by simp only [map_sub]
_ ≤ ‖L‖ * ‖g y‖ * ‖f p y - f q y‖ := (le_opNorm₂ _ _ _)
_ ≤ ‖L‖ * ‖g y‖ * δ := by gcongr
· simp only [hfs p y h'p hy, hfs q y hq hy, sub_self, norm_zero]
positivity
_ < ε := hδ
