English
If f: α → ℝ≥0 is measurable and μ is σ-finite, there exists a sequence of measurable sets s_n with finite measure that bound f by n on s_n and whose union is the whole space.
Русский
Если f: α → ℝ≥0 измерима и μ σ-конечной, существует последовательность измеримых множеств s_n с конечной мерой, на которых f ≤ n, и их объединение равно всему пространству.
LaTeX
$$$\\exists s : \\mathbb{N} \\to \\mathrm{Set}\\; \\alpha,\\ ( \\forall n, \\operatorname{MeasurableSet}(s(n)) \\wedge \\mu(s(n)) < \\infty \\wedge \\forall x \\in s(n), f(x) \\le n ) \\land \\bigcup_{i} s(i) = \\mathrm{Set.univ}$$$
Lean4
/-- If a function `f : α → ℝ≥0` is measurable and the measure is σ-finite, then there exists
spanning measurable sets with finite measure on which `f` is bounded.
See also `StronglyMeasurable.exists_spanning_measurableSet_norm_le` for functions into normed
groups. -/
theorem exists_spanning_measurableSet_le {f : α → ℝ≥0} (hf : Measurable f) (μ : Measure α) [SigmaFinite μ] :
∃ s : ℕ → Set α, (∀ n, MeasurableSet (s n) ∧ μ (s n) < ∞ ∧ ∀ x ∈ s n, f x ≤ n) ∧ ⋃ i, s i = Set.univ :=
by
let sigma_finite_sets := spanningSets μ
let norm_sets := fun n : ℕ => {x | f x ≤ n}
have norm_sets_spanning : ⋃ n, norm_sets n = Set.univ :=
by
ext1 x
simp only [Set.mem_iUnion, Set.mem_univ, iff_true]
exact exists_nat_ge (f x)
let sets n := sigma_finite_sets n ∩ norm_sets n
have h_meas : ∀ n, MeasurableSet (sets n) :=
by
refine fun n => MeasurableSet.inter ?_ ?_
· exact measurableSet_spanningSets μ n
· exact hf measurableSet_Iic
have h_finite : ∀ n, μ (sets n) < ∞ :=
by
refine fun n => (measure_mono Set.inter_subset_left).trans_lt ?_
exact measure_spanningSets_lt_top μ n
refine ⟨sets, fun n => ⟨h_meas n, h_finite n, ?_⟩, ?_⟩
· exact fun x hx => hx.2
· have : ⋃ i, sigma_finite_sets i ∩ norm_sets i = (⋃ i, sigma_finite_sets i) ∩ ⋃ i, norm_sets i :=
by
refine Set.iUnion_inter_of_monotone (monotone_spanningSets μ) fun i j hij x => ?_
simp only [norm_sets, Set.mem_setOf_eq]
refine fun hif => hif.trans ?_
exact mod_cast hij
rw [this, norm_sets_spanning, iUnion_spanningSets μ, Set.inter_univ]
