English
If a sequence of measurable functions f_i is given on a countable index set, their pointwise supremum is measurable.
Русский
Если имеется счетный набор измеримых функций f_i, их точечная мощность верхняя (sup) измерима.
LaTeX
$$∀ i, Measurable (f i) → Measurable (fun b => iSup fun i => f i b)$$
Lean4
@[measurability, fun_prop]
protected theorem iSup {ι} [Countable ι] {f : ι → δ → α} (hf : ∀ i, Measurable (f i)) :
Measurable (fun b ↦ ⨆ i, f i b) := by
rcases isEmpty_or_nonempty ι with hι | hι
· simp [iSup_of_empty']
have A : MeasurableSet {b | BddAbove (range (fun i ↦ f i b))} := measurableSet_bddAbove_range hf
have : Measurable (fun (_b : δ) ↦ sSup (∅ : Set α)) := measurable_const
apply Measurable.isLUB_of_mem hf A _ _ this
· intro b hb
apply isLUB_ciSup
simpa
· intro b hb
apply csSup_of_not_bddAbove
simpa
-- TODO: Why does this error?
-- /-- Compositional version of `Measurable.iSup` for use by `fun_prop`. -/
-- @[fun_prop]
-- protected lemma Measurable.iSup'' {_ : MeasurableSpace γ} {ι : Sort*} [Countable ι]
-- {f : ι → γ → δ → α} {h : γ → δ} (hf : ∀ i, Measurable ↿(f i)) (hh : Measurable h) :
-- Measurable fun a ↦ (⨆ i, f i a) (h a) := by
-- simp_rw [iSup_apply]
-- exact .iSup fun i ↦ by fun_prop
