English
Let μ be a measure and T a dominated finite‑additive family of linear maps. If f is integrable and measurable, and s is a subset of E that is separable, with a point y0 in s and the constant function y0 integrable, then the sequence of finite‑approximation setToFun(μ, T, hT, approxOn f, s, y0, h0) converges to setToFun(μ, T, hT, f) as the approximations get finer, i.e., Tendsto ... to setToFun μ T hT f.
Русский
Пусть μ — мера, T — семья ограниченно аддитивных линейных отображений, задаваемая на множествах α. Пусть f: α → E интегрируема и измерима, s ⊆ E такое, что имеет сепарабельность, выбраны y0 ∈ s и интегрируемая константа y0. Тогда последовательность приближений setToFun μ T hT (SimpleFunc.approxOn f ... n) сходится к setToFun μ T hT f при n → ∞.
LaTeX
$$$\\operatorname{Tendsto}\\left( n \\mapsto \\operatorname{setToFun} \\;\\mu\\; T\\; hT\\; (\\mathrm{SimpleFunc.approxOn} \\, f \\, hfm \\, s \\, y_0 \\, h_0 \\, n) \\right)\\;_{n \\to \\infty} \\; \\mathcal{N}\\left( \\operatorname{setToFun} \\;\\mu\\; T\\; hT\\; f \\right) $$$
Lean4
theorem tendsto_setToFun_approxOn_of_measurable (hT : DominatedFinMeasAdditive μ T C) [MeasurableSpace E] [BorelSpace E]
{f : α → E} {s : Set E} [SeparableSpace s] (hfi : Integrable f μ) (hfm : Measurable f)
(hs : ∀ᵐ x ∂μ, f x ∈ closure s) {y₀ : E} (h₀ : y₀ ∈ s) (h₀i : Integrable (fun _ => y₀) μ) :
Tendsto (fun n => setToFun μ T hT (SimpleFunc.approxOn f hfm s y₀ h₀ n)) atTop (𝓝 <| setToFun μ T hT f) :=
tendsto_setToFun_of_L1 hT _ hfi (Eventually.of_forall (SimpleFunc.integrable_approxOn hfm hfi h₀ h₀i))
(SimpleFunc.tendsto_approxOn_L1_enorm hfm _ hs (hfi.sub h₀i).2)
