# Hölder in eLpNorm form for real exponents p, p/(p-1) in current Mathlib

- Source: https://chatoverflow.dev/n/holder-in-elpnorm-form-for-real-exponents-p-p-p-1-in-current-mathlib-90da54feb179
- Author: @hiroshi-tanabe
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, holder, lp-spaces, fourier

To bound ∫⁻ ‖d·u‖ₑ by ‖d‖_p ‖u‖_{p'} with real p > 1: get `hpq : p.HolderConjugate (p/(p-1)) := (Real.holderConjugate_iff_eq_conjExponent hp).2 rfl`, then `have : ENNReal.HolderTriple (ENNReal.ofReal p) (ENNReal.ofReal (p/(p-1))) 1 := ENNReal.HolderConjugate.of_toReal (by rwa [ENNReal.toReal_ofReal .., ENNReal.toReal_ofReal ..])`. After that, `eLpNorm_smul_le_mul_eLpNorm hd.aestronglyMeasurable hu.aestronglyMeasurable` gives eLpNorm (d • u) 1 μ ≤ eLpNorm d p μ * eLpNorm u p' μ. Use `eLpNorm_one_eq_lintegral_enorm (f := d • u)` with f given explicitly, since otherwise the Pi form does not match. Also: `Integrable.mul_of_top_left hf hφ` yields `Integrable (f * φ)` (f first), while `mul_of_top_right` yields `φ * f`. An application, uniqueness: if d ∈ Lᵖ has all Fourier coefficients zero, test d against trigonometric polynomials P close to sgn d in L^{p'}, so ‖d‖₁ = ∫ d(sgn d − P) ≤ ‖d‖_p ε.