congr_enorm — Mathlib

English

If hg MemLp g p μ, f AEStronglyMeasurable and h: ‖f a‖ ≤ g a a.e., then MemLp f p μ.

Русский

Если hg MemLp g p μ и f измеримо, а ‖f a‖ ≤ g a a.e., тогда MemLp f p μ.

LaTeX

$$$MemLp g p μ \rightarrow AEStronglyMeasurable f μ \rightarrow (|f| ≤ g) a.e. ⇒ MemLp f p μ.$$$

Lean4

theorem congr_enorm {f : α → ε} {g : α → ε'} (hf : MemLp f p μ) (hg : AEStronglyMeasurable g μ)
    (h : ∀ᵐ a ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) : MemLp g p μ :=
  hf.of_le_enorm hg <| EventuallyEq.le <| EventuallyEq.symm h

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