holderConjugate_one_div

Mathlib.Data.Real.ConjExponents

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

← MathLib Explorer

English

For a,b > 0 with a + b = 1, (1/a).HolderConjugate (1/b).

Русский

Для a,b > 0 и a + b = 1, (1/a) и (1/b) — сопряжённые Холдеру.

LaTeX

$$(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