English
Given a measurable set s and a strongly measurable function f, there exists a sequence of simple functions fs_n supported on s that converge pointwise to f, and fs_n vanishes outside s.
Русский
Для измеримого множества s и сильно измеримой функции f существует последовательность простых функций, поддержанных на s, сходящаяся по точкам к f, и равная нулю вне s.
LaTeX
$$$\exists f_n: \mathbb{N} \to \alpha \to_s \beta, \; (\forall x, Tendssto_{n\to\infty} f_n(x)=f(x)) \land (\forall x\notin s, \forall n, f_n(x)=0)$$$
Lean4
theorem stronglyMeasurable_in_set {m : MeasurableSpace α} [TopologicalSpace β] [Zero β] {s : Set α} {f : α → β}
(hs : MeasurableSet s) (hf : StronglyMeasurable f) (hf_zero : ∀ x, x ∉ s → f x = 0) :
∃ fs : ℕ → α →ₛ β, (∀ x, Tendsto (fun n => fs n x) atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ n, fs n x = 0 :=
by
let g_seq_s : ℕ → @SimpleFunc α m β := fun n => (hf.approx n).restrict s
have hg_eq : ∀ x ∈ s, ∀ n, g_seq_s n x = hf.approx n x :=
by
intro x hx n
rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_mem hx]
have hg_zero : ∀ x ∉ s, ∀ n, g_seq_s n x = 0 := by
intro x hx n
rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_notMem hx]
refine ⟨g_seq_s, fun x => ?_, hg_zero⟩
by_cases hx : x ∈ s
· simp_rw [hg_eq x hx]
exact hf.tendsto_approx x
· simp_rw [hg_zero x hx, hf_zero x hx]
exact tendsto_const_nhds
