nnnorm_indicatorConstLp_le — Mathlib

English

The norm of indicatorConstLp is bounded above by the right-hand side: ||indicatorConstLp(p, hs, hμs, c)|| ≤ ||c|| μ(s)^{1/p}.

Русский

Норма indicatorConstLp ограничена сверху правой частью: ||indicatorConstLp(p, hs, hμs, c)|| ≤ ||c|| μ(s)^{1/p}.

LaTeX

$$$\|indicatorConstLp(p, hs, hμs, c)\| ≤ \|c\| \cdot μ(s)^{1/p^{real}}.$$$

Lean4

theorem nnnorm_indicatorConstLp_le : ‖indicatorConstLp p hs hμs c‖₊ ≤ ‖c‖₊ * (μ s).toNNReal ^ (1 / p.toReal) :=
  norm_indicatorConstLp_le

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