English
If s is a countable index set and each f_i is AEMeasurable, then the double-supremum over i and a part of i is AEMeasurable.
Русский
Если s — счетный индексный набор и каждая f_i — AEMeasurable, то двойной суперпоследовательность над i и частью индекса — AEMeasurable.
LaTeX
$$s.Countable → (∀ i ∈ s, AEMeasurable (f i) μ) → AEMeasurable (fun b => iSup fun i => iSup fun h => f i b) μ$$
Lean4
theorem biSup {ι} {μ : Measure δ} (s : Set ι) {f : ι → δ → α} (hs : s.Countable) (hf : ∀ i ∈ s, AEMeasurable (f i) μ) :
AEMeasurable (fun b => ⨆ i ∈ s, f i b) μ := by
classical
let g : ι → δ → α := fun i ↦ if hi : i ∈ s then (hf i hi).mk (f i) else fun _b ↦ sSup ∅
have : ∀ i ∈ s, Measurable (g i) := by
intro i hi
simpa [g, hi] using (hf i hi).measurable_mk
refine ⟨fun b ↦ ⨆ (i) (_ : i ∈ s), g i b, .biSup s hs this, ?_⟩
have : ∀ i ∈ s, ∀ᵐ b ∂μ, f i b = g i b := fun i hi ↦ by simpa [g, hi] using (hf i hi).ae_eq_mk
filter_upwards [(ae_ball_iff hs).2 this] with b hb
exact iSup_congr fun i => iSup_congr (hb i)
