English
If a sequence f n lies in measurableLE(μ, ν) for each n, then the function a↦⨆_{k≤n} f_k(a) lies in measurableLE(μ, ν) for every n.
Русский
Если для каждого n функция f_n принадлежит measurableLE(μ, ν), то функция a↦ sup_{k≤n} f_k(a) принадлежит measurableLE(μ, ν) для любого n.
LaTeX
$$$$ (\\forall n, f_n \\in \\mathrm{measurableLE}(\\mu, \\nu)) \\Rightarrow (\\forall n, \\; (\\,a \\mapsto \\big(\\bigvee_{k \\le n} f_k(a)\\big) ) \\in \\mathrm{measurableLE}(\\mu, \\nu)). $$$$
Lean4
theorem iSup_mem_measurableLE (f : ℕ → α → ℝ≥0∞) (hf : ∀ n, f n ∈ measurableLE μ ν) (n : ℕ) :
(fun x ↦ ⨆ (k) (_ : k ≤ n), f k x) ∈ measurableLE μ ν := by
induction n with
| zero =>
constructor
· simp [(hf 0).1]
· intro A hA; simp [(hf 0).2 A hA]
| succ m
hm =>
have : (fun a : α ↦ ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a) = fun a ↦ f m.succ a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a :=
funext fun _ ↦ iSup_succ_eq_sup _ _ _
refine ⟨.iSup fun n ↦ Measurable.iSup_Prop _ (hf n).1, fun A hA ↦ ?_⟩
rw [this]; exact (sup_mem_measurableLE (hf m.succ) hm).2 A hA
