eLpNorm_star — Mathlib

English

For a star-structure, eLpNorm is invariant under taking star of the function: eLpNorm(f star) = eLpNorm(f).

Русский

Норма eLp не изменяется при операции взятия звезды: eLpNorm(star f) = eLpNorm(f).

LaTeX

$$$$eLpNorm(star f)_{p} = eLpNorm(f)_{p}.$$$$

Lean4

@[simp]
theorem eLpNorm_star {p : ℝ≥0∞} {f : α →ₘ[μ] R} : eLpNorm (star f : α →ₘ[μ] R) p μ = eLpNorm f p μ :=
  eLpNorm_congr_ae (coeFn_star f) |>.trans <| by simp

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