ae_eq — Mathlib

English

If f is UnifIntegrable and f_n equals g_n a.e., then g is UnifIntegrable; conversely with the symmetric equality.

Русский

Если f — UnifIntegrable и f_n совпадает с g_n почти везде, тогда g — UnifIntegrable; и наоборот.

LaTeX

$$$\\forall n, f_n =_{μ}^{a.e.} g_n \\Rightarrow \\operatorname{UnifIntegrable} g p μ$$$

Lean4

protected theorem ae_eq (hf : UnifIntegrable f p μ) (hfg : ∀ n, f n =ᵐ[μ] g n) : UnifIntegrable g p μ := by
  classical
  intro ε hε
  obtain ⟨δ, hδ_pos, hfδ⟩ := hf hε
  refine ⟨δ, hδ_pos, fun n s hs hμs => (le_of_eq <| eLpNorm_congr_ae ?_).trans (hfδ n s hs hμs)⟩
  filter_upwards [hfg n] with x hx
  simp_rw [Set.indicator_apply, hx]

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