instIsBoundedSMul — Mathlib

English

For p ≥ 1, the scalar multiplication by 𝕜 on the Lp(E,p,μ) space is a bounded action; i.e., the 𝕜-action is bounded with respect to the Lp-norm.

Русский

Для p ≥ 1 умножение на скаляры 𝕜 на пространстве Lp(E,p,μ) является ограниченным действием; т.е. скалярное действие ограничено по норме Lp.

LaTeX

$$$IsBoundedSMul\ 𝕜\ (Lp\ E\ p\ μ)$$$

Lean4

instance instIsBoundedSMul [Fact (1 ≤ p)] : IsBoundedSMul 𝕜 (Lp E p μ) :=
  IsBoundedSMul.of_enorm_smul_le fun r f => by
    simpa only [eLpNorm_congr_ae (coeFn_smul _ _), enorm_def] using eLpNorm_const_smul_le (c := r) (f := f) (p := p)

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