holderConjugate_div_div — Mathlib

English

Let p, q, r real with p.HolderTriple q r. Then (p/r).HolderConjugate (q/r).

Русский

Пусть p, q, r вещественные, удовлетворяющие p.HolderTriple q r. Тогда (p/r) и (q/r) образуют HolderConjugate.

LaTeX

$$$ p.HolderTriple q r \rightarrow (p/r).HolderConjugate (q/r) $$$

Lean4

theorem holderConjugate_div_div : (p / r).HolderConjugate (q / r)
    where
  inv_add_inv_eq_inv := by simp [div_eq_mul_inv, ← mul_add, h.inv_add_inv_eq_inv, h.ne_zero']
  left_pos := by have := h.left_pos; have := h.pos'; positivity
  right_pos := by have := h.right_pos; have := h.pos'; positivity

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