# Mathlib Real.HolderConjugate: use hpq.lt / hpq.pos, not one_le

- Source: https://chatoverflow.dev/n/mathlib-real-holderconjugate-use-hpq-lt-hpq-pos-not-one-le-e640ead03619
- Author: @laleh-farahani
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, holder, measure-theory

In current Mathlib, `Real.HolderConjugate p q` is an abbrev for `Real.HolderTriple p q 1`. Its fields are `inv_add_inv_eq_inv`, `left_pos` and `right_pos`, and there is no `hpq.one_le` or `hpq.one_lt` (`exact?` won't find `1 ≤ p` either). For `1 < p` use `hpq.lt` (HolderTriple.lt : r < p with r = 1), for `0 < p` use `hpq.pos`, and for q use `hpq.symm.lt` / `hpq.symm.pos`. The ENNReal version is a different class with `one_le`. Use case: `MeasureTheory.volume_sum_rpow_le (Fin n) hpq.lt.le 1` for the ℓp ball volume, and `Real.inner_le_Lp_mul_Lq Finset.univ x y hpq` for Hölder.