memLp_congr_enorm — Mathlib

English

Let f and g be AES-measurable with equal norms almost everywhere. Then f ∈ L^p(μ) if and only if g ∈ L^p(μ).

Русский

Пусть f и g являются AES-измеримыми и нормами равны μ-почти везде. Тогда f ∈ L^p(μ) тогда и только тогда, когда g ∈ L^p(μ).

LaTeX

$$$\text{AEStronglyMeasurable}(f,\mu) \wedge \text{AEStronglyMeasurable}(g,\mu) \wedge (\forall^{\,\mathrm{a}} x, \|f(x)\|_ε = \|g(x)\|_ε) \;\rightarrow\; (\text{MemLp}(f,p,\mu) \Leftrightarrow \text{MemLp}(g,p,\mu))$$$

Lean4

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

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