holderConjugate_iff_eq_conjExponent

English

For p > 1, p.HolderConjugate q holds if and only if q = p/(p−1).

Русский

Для p > 1 верно: p.HolderConjugate q тогда и только тогда, когда q = p/(p−1).

LaTeX

$$$p > 1 \Rightarrow (p.HolderConjugate q \iff q = \dfrac{p}{p-1})$$$

Lean4

theorem holderConjugate_iff_eq_conjExponent (hp : 1 < p) : p.HolderConjugate q ↔ q = p / (p - 1) :=
  ⟨HolderConjugate.conjugate_eq, fun h ↦ holderConjugate_iff.mpr ⟨hp, by simp [field, h]⟩⟩

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