ae_eq — Mathlib

English

If two families f and g are a.e. equal, then UniformIntegrable f and UniformIntegrable g have the same property; i.e., ae-equality transfers uniform integrability.

Русский

Если две последовательности функций совпадают почти всюду, то их UniformIntegrable свойства совпадают; сохранение через a.e.-равенство.

LaTeX

$$$\forall i,\ f_i =_{ae} g_i \Rightarrow UniformIntegrable f p μ \iff UniformIntegrable g p μ$$$

Lean4

theorem ae_eq {g : ι → α → β} (hf : UniformIntegrable f p μ) (hfg : ∀ n, f n =ᵐ[μ] g n) : UniformIntegrable g p μ :=
  by
  obtain ⟨hfm, hunif, C, hC⟩ := hf
  refine ⟨fun i => (hfm i).congr (hfg i), (unifIntegrable_congr_ae hfg).1 hunif, C, fun i => ?_⟩
  rw [← eLpNorm_congr_ae (hfg i)]
  exact hC i

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