congr' — Mathlib

English

If f is integrable and g is AEStronglyMeasurable with ∥f∥ = ∥g∥ a.e., then g is integrable.

Русский

Если f интегрируемо и g AEStronglyMeasurable с almost everywhere равенством норм ∥f∥ = ∥g∥, то g интегрируемо.

LaTeX

$$$\operatorname{Integrable}(f, \mu) \wedge \operatorname{AEStronglyMeasurable}(g, \mu) \wedge (\forall^\mathrm{ae} a, \|f(a)\| = \|g(a)\|) \Rightarrow \operatorname{Integrable}(g, \mu)$$$

Lean4

theorem congr' {f : α → β} {g : α → γ} (hf : Integrable f μ) (hg : AEStronglyMeasurable g μ)
    (h : ∀ᵐ a ∂μ, ‖f a‖ = ‖g a‖) : Integrable g μ :=
  ⟨hg, hf.hasFiniteIntegral.congr' h⟩

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