norm_holderL_le

Mathlib.MeasureTheory.Function.Holder

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.norm_holderL_le

English

The operator norm of HolderL is bounded by the operator norm of B with Holder conjugates in play.

Русский

Норма оператора HolderL ограничена нормой оператора B с учетом сопряжённости Холдэра.

LaTeX

$$$\\|\\mathrm{holderL}(B)\\|_{op} \\le \\|B\\|_{op}.$$$

Lean4

theorem norm_holderL_le : ‖(B.holderL μ p q r)‖ ≤ ‖B‖ :=
  LinearMap.mkContinuous₂_norm_le _ (norm_nonneg B) _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru