toReal_iff — Mathlib

English

For hp > 1, p.toReal.HolderConjugate q.toReal iff p.HolderConjugate q.

Русский

Для hp > 1, p.toReal.HolderConjugate q.toReal эквивалентно p.HolderConjugate q.

LaTeX

$$$p.toReal.HolderConjugate q.toReal \\iff p.HolderConjugate q$$$

Lean4

theorem toReal_iff (hp : 1 < p.toReal) : p.toReal.HolderConjugate q.toReal ↔ p.HolderConjugate q :=
  by
  refine ⟨of_toReal, fun h ↦ ?_⟩
  have hq : 0 < q.toReal := by
    rw [toReal_pos_iff]
    refine ⟨pos q p, lt_top_iff_one_lt q p |>.mpr ?_⟩
    contrapose! hp
    exact toReal_mono one_ne_top hp
  simpa using HolderTriple.toReal 1 (zero_lt_one.trans hp) hq

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