holderConjugate_iff_eq_conjExponent

English

Holder conjugate equivalence: p.HolderConjugate q ⇔ 1 < p ∧ p^{-1} + q^{-1} = 1.

Русский

Эквивалентность сопряжения Холдера: p.HolderConjugate q ⇔ 1 < p ∧ p^{-1} + q^{-1} = 1.

LaTeX

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

Lean4

theorem holderConjugate_iff_eq_conjExponent (hp : 1 < p) : p.HolderConjugate q ↔ q = p / (p - 1) :=
  by
  rw [← holderConjugate_coe_iff, Real.holderConjugate_iff_eq_conjExponent (by exact_mod_cast hp), ← coe_one, ←
    NNReal.coe_sub hp.le]
  exact_mod_cast Iff.rfl

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