Theorems · Definition · real analysis

NNReal.HolderConjugate

NNReal → NNReal → Prop

Nonnegative real numbers p q : ℝ≥0 are Hölder conjugate if they are positive and satisfy the equality p⁻¹ + q⁻¹ = 1. This is an abbreviation for NNReal.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 NNReal.holderConjugate_iff.

Defined in

Mathlib.Data.Real.ConjExponents

Cited by

33 results in Mathlib

Foundations

Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound