holderConjugate_one_div

Mathlib.Data.Real.ConjExponents

URI: https://scilib.ai/kg/mathlib#Real.holderConjugate_one_div

← MathLib Explorer

English

For a,b > 0 with a+b=1, (1/a) and (1/b) are Holder conjugates.

Русский

Для a,b > 0 с a+b=1 числа 1/a и 1/b сопряжены Холдером.

LaTeX

$$$(a > 0) \land (b > 0) \land (a + b = 1) \Rightarrow (1 / a) \HolderConjugate (1 / b)$$$

Lean4

theorem holderConjugate_one_div (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) : (1 / a).HolderConjugate (1 / b) := by
  simpa using HolderConjugate.inv_inv ha hb hab

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

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

Разделы

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

Аффилиация

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