holderConjugate_iff

Mathlib.Data.ENNReal.Holder

URI: https://scilib.ai/kg/mathlib#ENNReal.holderConjugate_iff

English

For p,q ∈ ENNReal, the Holder conjugate of p and q holds if and only if p^{-1} + q^{-1} = 1.

Русский

Для p,q ∈ ENNReal сопряжение Холдера выполняется тогда и только тогда, когда p^{-1} + q^{-1} = 1.

LaTeX

$$HolderConjugate(p,q) \iff p^{-1} + q^{-1} = 1$$

Lean4

theorem holderConjugate_iff {p q : ℝ≥0∞} : HolderConjugate p q ↔ p⁻¹ + q⁻¹ = 1 := by simp [holderTriple_iff]

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

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

Разделы

Аффилиация

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