integrable_congr' — Mathlib

English

If AEStronglyMeasurable f and g are a.e. equal in norm, then integrability of f and g are equivalent.

Русский

Если AEStronglyMeasurable f и g равны по норме почти всюду, то интегрируемость f и g эквивалентны.

LaTeX

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

Lean4

theorem integrable_congr' {f : α → β} {g : α → γ} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ)
    (h : ∀ᵐ a ∂μ, ‖f a‖ = ‖g a‖) : Integrable f μ ↔ Integrable g μ :=
  integrable_congr'_enorm hf hg <| h.mono fun _x hx ↦ enorm_eq_iff_norm_eq.mpr hx

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