English
A specialized variant: when f_i are measurable and g is LUB a.e. on each measurable set, then g is measurable.
Русский
Специализированный вариант: если f_i измеримы и g является a.e. LUB на каждой измеримой множестве, то g измерима.
LaTeX
$$$\forall i,\text{Measurable}(f_i) \Rightarrow \forall s, \text{MeasurableSet}(s) \Rightarrow (\forall b \in s, IsLUB(\{a: a=f_i(b)\}) (g(b))) \Rightarrow \text{Measurable}(g)$$$
Lean4
/-- If a function is the least upper bound of countably many measurable functions on a measurable
set `s`, and coincides with a measurable function outside of `s`, then it is measurable. -/
theorem isLUB_of_mem {ι} [Countable ι] {f : ι → δ → α} {g g' : δ → α} (hf : ∀ i, Measurable (f i)) {s : Set δ}
(hs : MeasurableSet s) (hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)) (hg' : EqOn g g' sᶜ)
(g'_meas : Measurable g') : Measurable g := by
classical
rcases isEmpty_or_nonempty ι with hι | ⟨⟨i⟩⟩
· rcases eq_empty_or_nonempty s with rfl | ⟨x, hx⟩
· convert g'_meas
rwa [compl_empty, eqOn_univ] at hg'
· have A : ∀ b ∈ s, IsBot (g b) := by simpa using hg
have B : ∀ b ∈ s, g b = g x := by
intro b hb
apply le_antisymm (A b hb (g x)) (A x hx (g b))
have : g = s.piecewise (fun _y ↦ g x) g' := by
ext b
by_cases hb : b ∈ s
· simp [hb, B]
· simp [hb, hg' hb]
rw [this]
exact Measurable.piecewise hs measurable_const g'_meas
· have : Nonempty ι := ⟨i⟩
let f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
suffices ∀ b, IsLUB {a | ∃ i, f' i b = a} (g b) from
Measurable.isLUB (fun i ↦ Measurable.piecewise hs (hf i) g'_meas) this
intro b
by_cases hb : b ∈ s
· have A : ∀ i, f' i b = f i b := fun i ↦ by simp [f', hb]
simpa [A] using hg b hb
· have A : ∀ i, f' i b = g' b := fun i ↦ by simp [f', hb]
simp [A, hg' hb, isLUB_singleton]
