memLp_congr_norm — Mathlib

English

If AES-measurable f and g satisfy that their norms coincide almost everywhere, then membership in L^p is equivalent for f and g.

Русский

Если у функций f и g равны нормы μ-почти везде, то принадлежность к L^p одинакова для f и g.

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_norm {f : α → E} {g : α → F} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ)
    (h : ∀ᵐ a ∂μ, ‖f a‖ = ‖g a‖) : MemLp f p μ ↔ MemLp g p μ :=
  ⟨fun h2f => h2f.congr_norm hg h, fun h2g => h2g.congr_norm hf <| EventuallyEq.symm h⟩

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