conjugate_eq

Mathlib.Data.Real.ConjExponents

URI: https://scilib.ai/kg/mathlib#NNReal.HolderConjugate.conjugate_eq

← MathLib Explorer

English

Let p and q be Holder conjugates. Then q = p/(p − 1).

Русский

Пусть p и q — сопряжённые Холдеру. Тогда q = p/(p − 1).

LaTeX

$$$q = \\dfrac{p}{p-1}$$$

Lean4

theorem conjugate_eq : q = p / (p - 1) :=
  by
  have : ((1 : ℝ≥0) : ℝ) ≤ p := h.coe.lt.le
  exact_mod_cast NNReal.coe_sub this ▸ coe_one ▸ h.coe.conjugate_eq

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

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

Разделы

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

Аффилиация

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