holderConjugate_iff — Mathlib

English

For all p, q ∈ Real, p.HolderConjugate q holds if and only if 1 < p and p^{-1} + q^{-1} = 1.

Русский

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

LaTeX

$$$p.HolderConjugate q \iff (1 < p \land p^{-1} + q^{-1} = 1)$$$

Lean4

theorem _root_.Real.holderConjugate_iff : p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1 :=
  by
  refine ⟨fun h ↦ ⟨h.lt, h.inv_add_inv_eq_one⟩, ?_⟩
  rintro ⟨hp, h⟩
  have hp' := zero_lt_one.trans hp
  refine ⟨inv_one (G := ℝ) |>.symm ▸ h, hp', ?_⟩
  rw [← inv_lt_one₀ hp', ← sub_pos] at hp
  exact inv_pos.mp <| eq_sub_of_add_eq' h ▸ hp

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