holderConjugate_div_div — Mathlib

English

If p, q, r ∈ ENNReal satisfy HolderTriple p q r and r ≠ 0, ∞, then HolderConjugate (p/r) (q/r).

Русский

Если p, q, r ∈ ENNReal удовлетворяют HolderTriple p q r и r ≠ 0, ∞, то HolderConjugate (p/r) (q/r).

LaTeX

$$$HolderTriple(p,q,r) \land r \neq 0 \land r \neq \infty \Rightarrow HolderConjugate \left(\frac{p}{r}\right)\left(\frac{q}{r}\right)$$$

Lean4

theorem holderConjugate_div_div (hr₀ : r ≠ 0) (hr : r ≠ ∞) : HolderConjugate (p / r) (q / r) where
  inv_add_inv_eq_inv := by
    rw [ENNReal.inv_div (.inl hr) (.inl hr₀), ENNReal.inv_div (.inl hr) (.inl hr₀), div_eq_mul_inv, div_eq_mul_inv, ←
      mul_add, inv_add_inv_eq_inv p q r, ENNReal.mul_inv_cancel hr₀ hr, inv_one]

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