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

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 ε.