holderConjugate_div_div — Mathlib

English

If p,q,r form a Holder triple, then (p/r) and (q/r) are Holder conjugates; equivalently, (p/r)^{-1} + (q/r)^{-1} = 1.

Русский

Если p, q, r образуют тройку Холдера, то (p/r) и (q/r) являются конъюгатами Холдера; эквивалентно (p/r)^{-1} + (q/r)^{-1} = 1.

LaTeX

$$$(p/r)^{-1} + (q/r)^{-1} = 1$$$

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

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