holderConjugate_iff — Mathlib

English

Holder conjugate holds iff p > 1 and p^{-1} + q^{-1} = 1.

Русский

Сопряжённость Холдера сохраняется тогда и только тогда, когда p > 1 и p^{-1} + q^{-1} = 1.

LaTeX

$$p.HolderConjugate q \\Leftrightarrow 1 < p \\wedge p^{-1} + q^{-1} = 1$$

Lean4

theorem _root_.NNReal.holderConjugate_iff : p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1 :=
  by
  rw [← holderConjugate_coe_iff, Real.holderConjugate_iff, ← coe_one]
  exact_mod_cast Iff.rfl

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