uniformIntegrable_congr_ae — Mathlib

English

UniformIntegrable is preserved under ae-congruence: if f equals g almost everywhere, then UniformIntegrable f and UniformIntegrable g are equivalent.

Русский

UniformIntegrable сохраняется под ae-эквивалентностью: если f ≈ g почти везде, то UniformIntegrable f и UniformIntegrable g эквивалентны.

LaTeX

$$$UniformIntegrable f p μ \iff UniformIntegrable g p μ$ под условием $f =_{ae} g$$$

Lean4

theorem uniformIntegrable_congr_ae {g : ι → α → β} (hfg : ∀ n, f n =ᵐ[μ] g n) :
    UniformIntegrable f p μ ↔ UniformIntegrable g p μ :=
  ⟨fun h => h.ae_eq hfg, fun h => h.ae_eq fun i => (hfg i).symm⟩

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