HolderConjugate — Mathlib

English

HolderConjugate p q is defined as HolderTriple p q 1.

Русский

HolderConjugate p q определяется как HolderTriple p q 1.

LaTeX

$$$\mathrm{HolderConjugate}(p,q) = \mathrm{HolderTriple}(p,q,1)$$$

Lean4

/-- Real numbers `p q : ℝ` are **Hölder conjugate** if they are positive and satisfy the
equality `p⁻¹ + q⁻¹ = 1`. This is an abbreviation for `Real.HolderTriple p q 1`. This condition
shows up in many theorems in analysis, notably related to `L^p` norms.

It is equivalent that `1 < p` and `p⁻¹ + q⁻¹ = 1`. See `Real.holderConjugate_iff`. -/
abbrev HolderConjugate (p q : ℝ) :=
  HolderTriple p q 1

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