English
For a strongly measurable function, there exist spanning measurable sets with finite measure on which the function is bounded; the union of these sets covers the whole space.
Русский
Для сильно измеримой функции существуют покрывающие множества измеримые с конечной мерой, на которых функция ограничена; их объединение покрывает всю пространство.
LaTeX
$$$\exists s_n: \mathbb{N} \to \text{MeasurableSet}, \ μ(s_n) < \infty, \|f(x)\| \le n \text{ for } x\in s_n, \bigcup_n s_n = \alpha$$$
Lean4
/-- If a function `f` is strongly measurable w.r.t. a sub-σ-algebra `m` and the measure is σ-finite
on `m`, then there exists spanning measurable sets with finite measure on which `f` has bounded
norm. In particular, `f` is integrable on each of those sets. -/
theorem exists_spanning_measurableSet_norm_le [SeminormedAddCommGroup β] {m m0 : MeasurableSpace α} (hm : m ≤ m0)
(hf : StronglyMeasurable[m] f) (μ : Measure α) [SigmaFinite (μ.trim hm)] :
∃ s : ℕ → Set α, (∀ n, MeasurableSet[m] (s n) ∧ μ (s n) < ∞ ∧ ∀ x ∈ s n, ‖f x‖ ≤ n) ∧ ⋃ i, s i = Set.univ :=
by
obtain ⟨s, hs, hs_univ⟩ := @exists_spanning_measurableSet_le _ m _ hf.nnnorm.measurable (μ.trim hm) _
refine ⟨s, fun n ↦ ⟨(hs n).1, (le_trim hm).trans_lt (hs n).2.1, fun x hx ↦ ?_⟩, hs_univ⟩
have hx_nnnorm : ‖f x‖₊ ≤ n := (hs n).2.2 x hx
rw [← coe_nnnorm]
norm_cast
