LpAddConst

Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality

URI: https://scilib.ai/kg/mathlib#MeasureTheory.LpAddConst

← MathLib Explorer

English

LpAddConst(0) = 1.

Русский

LpAddConst(0) = 1.

LaTeX

$$$\\operatorname{LpAddConst}(0) = 1$$$

Lean4

/-- A constant for the inequality `‖f + g‖_{L^p} ≤ C * (‖f‖_{L^p} + ‖g‖_{L^p})`. It is equal to `1`
for `p ≥ 1` or `p = 0`, and `2^(1/p-1)` in the more tricky interval `(0, 1)`. -/
noncomputable def LpAddConst (p : ℝ≥0∞) : ℝ≥0∞ :=
  if p ∈ Set.Ioo (0 : ℝ≥0∞) 1 then (2 : ℝ≥0∞) ^ (1 / p.toReal - 1) else 1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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