English
In a second-countable space with sigma-finite measure, Finite Strongly Measurable is equivalent to Measurable.
Русский
В пространстве второго счёта с сигма-ограниченной мерой, конечная сильная измеримость эквивалентна измеримости.
LaTeX
$$$\text{FinStronglyMeasurable}(f,\mu) \iff \text{Measurable}(f)$$$
Lean4
theorem exists_set_sigmaFinite [Zero β] [TopologicalSpace β] [T2Space β] (hf : FinStronglyMeasurable f μ) :
∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t) :=
by
rcases hf with ⟨fs, hT_lt_top, h_approx⟩
let T n := support (fs n)
have hT_meas : ∀ n, MeasurableSet (T n) := fun n => SimpleFunc.measurableSet_support (fs n)
let t := ⋃ n, T n
refine ⟨t, MeasurableSet.iUnion hT_meas, ?_, ?_⟩
· have h_fs_zero : ∀ n, ∀ x ∈ tᶜ, fs n x = 0 := by
intro n x hxt
rw [Set.mem_compl_iff, Set.mem_iUnion, not_exists] at hxt
simpa [T] using hxt n
refine fun x hxt => tendsto_nhds_unique (h_approx x) ?_
rw [funext fun n => h_fs_zero n x hxt]
exact tendsto_const_nhds
· refine ⟨⟨⟨fun n => tᶜ ∪ T n, fun _ => trivial, fun n => ?_, ?_⟩⟩⟩
· rw [Measure.restrict_apply' (MeasurableSet.iUnion hT_meas), Set.union_inter_distrib_right, Set.compl_inter_self t,
Set.empty_union]
exact (measure_mono Set.inter_subset_left).trans_lt (hT_lt_top n)
· rw [← Set.union_iUnion tᶜ T]
exact Set.compl_union_self _
