integrable_congr'_enorm — Mathlib

English

If f is integrable and the ENorms of f and g are equal almost everywhere, then f and g are integrable equivalently.

Русский

Если f интегрируемо и ENorm(f) = ENorm(g) почти всюду, то f и g интегрируемы взаимно эквивалентно.

LaTeX

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

Lean4

theorem integrable_congr'_enorm {f : α → ε} {g : α → ε'} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ)
    (h : ∀ᵐ a ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) : Integrable f μ ↔ Integrable g μ :=
  ⟨fun h2f => h2f.congr'_enorm hg h, fun h2g => h2g.congr'_enorm hf <| EventuallyEq.symm h⟩

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