measurable_of_tendsto' — Mathlib

English

There is a MeasurableMul₂ structure on ENNReal, i.e., two-argument multiplication is measurable.

Русский

Двойная операция умножения ENNReal измерима.

LaTeX

$$$\text{MeasurableMul₂ ENNReal}$$$

Lean4

/-- A limit (over a general filter) of measurable `ℝ≥0∞`-valued functions is measurable. -/
theorem measurable_of_tendsto' {ι : Type*} {f : ι → α → ℝ≥0∞} {g : α → ℝ≥0∞} (u : Filter ι) [NeBot u]
    [IsCountablyGenerated u] (hf : ∀ i, Measurable (f i)) (lim : Tendsto f u (𝓝 g)) : Measurable g :=
  by
  rcases u.exists_seq_tendsto with ⟨x, hx⟩
  rw [tendsto_pi_nhds] at lim
  have : (fun y => liminf (fun n => (f (x n) y : ℝ≥0∞)) atTop) = g :=
    by
    ext1 y
    exact ((lim y).comp hx).liminf_eq
  rw [← this]
  change Measurable fun y => liminf (fun n => (f (x n) y : ℝ≥0∞)) atTop
  exact .liminf fun n => hf (x n)

Похожие утверждения