one_sub_inv_inv

Mathlib.Data.Real.ConjExponents

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

English

If 0 < a < 1, then (1 − a)^{-1} and a^{-1} are Holder conjugates.

Русский

Если 0 < a < 1, то (1 − a)^{-1} и a^{-1} — сопряжённые Холдеру.

LaTeX

$$(1 - a)^{-1}.HolderConjugate a^{-1}$$

Lean4

theorem one_sub_inv_inv (ha₀ : 0 < a) (ha₁ : a < 1) : (1 - a)⁻¹.HolderConjugate a⁻¹ :=
  (inv_one_sub_inv ha₀ ha₁).symm

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

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

Разделы

Аффилиация

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