eLpNorm'_congr_nnnorm_ae — Mathlib

English

If almost everywhere ‖f(x)‖₊ = ‖g(x)‖₊, then eLpNorm'(f,q,μ) = eLpNorm'(g,q,μ).

Русский

Если почти наверняка ‖f(x)‖₊ = ‖g(x)‖₊, то eLpNorm'(f,q,μ) = eLpNorm'(g,q,μ).

LaTeX

$$$\\ae x,\\|f(x)\\|_{nn} = \\|g(x)\\|_{nn} \\Rightarrow eLpNorm'(f,q,μ) = eLpNorm'(g,q,μ).$$$

Lean4

theorem eLpNorm'_congr_nnnorm_ae {f g : α → F} (hfg : ∀ᵐ x ∂μ, ‖f x‖₊ = ‖g x‖₊) : eLpNorm' f q μ = eLpNorm' g q μ :=
  by
  have : (‖f ·‖ₑ ^ q) =ᵐ[μ] (‖g ·‖ₑ ^ q) := hfg.mono fun x hx ↦ by simp [enorm, hx]
  simp only [eLpNorm'_eq_lintegral_enorm, lintegral_congr_ae this]

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