English
If fs x are measurable and bounded by bound on a neighborhood of x0 in s, and bound is integrable, then setToFun is continuous within s.
Русский
Если fs x ограничены и интегрируемы, то setToFun непрерывна внутри s.
LaTeX
$$$\\text{ContinuousWithinAt} (\\lambda x.\\mathrm{setToFun}(\\mu,T,hT,fs x))\\text{ on } s$$$
Lean4
theorem continuousOn_setToFun_of_dominated (hT : DominatedFinMeasAdditive μ T C) {fs : X → α → E} {bound : α → ℝ}
{s : Set X} (hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ) (h_bound : ∀ x ∈ s, ∀ᵐ a ∂μ, ‖fs x a‖ ≤ bound a)
(bound_integrable : Integrable bound μ) (h_cont : ∀ᵐ a ∂μ, ContinuousOn (fun x => fs x a) s) :
ContinuousOn (fun x => setToFun μ T hT (fs x)) s :=
by
intro x hx
refine continuousWithinAt_setToFun_of_dominated hT ?_ ?_ bound_integrable ?_
· filter_upwards [self_mem_nhdsWithin] with x hx using hfs_meas x hx
· filter_upwards [self_mem_nhdsWithin] with x hx using h_bound x hx
· filter_upwards [h_cont] with a ha using ha x hx
