Upgrade [`Real.exists_isMinOn_Gamma_Ioi`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.html#Real.exists_isMinOn_Gamma_Ioi) from an `∃` to an `∃!` by showing that the Gamma function is strictly-log-convex using the strict version of [Hölder's inequality](https://en.wikipedia.org/wiki/H%C3%B6lder%27s_inequality) (we only have log-convex).
Upgrade
Real.exists_isMinOn_Gamma_Ioifrom an∃to an∃!by showing that the Gamma function is strictly-log-convex using the strict version of Hölder's inequality (we only have log-convex).