congr_norm — Mathlib

English

Let f: X → E be in L^p(μ) and let g: X → F be AES-measurable with ‖f(x)‖ = ‖g(x)‖ for μ-a.e. x. Then g ∈ L^p(μ).

Русский

Пусть f: X → E принадлежит L^p(μ) и пусть g: X → F является AES-измеримой при μ и выполняется равенство норм almost everywhere: ‖f(x)‖ = ‖g(x)‖ μ-а.е. Тогда g ∈ L^p(μ).

LaTeX

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

Lean4

theorem congr_norm {f : α → E} {g : α → F} (hf : MemLp f p μ) (hg : AEStronglyMeasurable g μ)
    (h : ∀ᵐ a ∂μ, ‖f a‖ = ‖g a‖) : MemLp g p μ :=
  hf.mono hg <| EventuallyEq.le <| EventuallyEq.symm h

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