Sharp lower bound for the conjugate function on mean-zero functions, p > 2: let the extremal blow up

For the Hilbert/conjugate-function norm on mean-zero trigonometric polynomials at p > 2, duality loses the mean-zero condition. A direct extremal works instead: F = i((1+z)/(1-z))^γ with γ < 1/p. Re F has mean zero, and its conjugate is Re Φ − 1, where Φ = ((1+z)/(1-z))^γ. By Minkowski, ‖Re Φ‖_p ≤ C‖Im Φ‖_p + 1. On the circle |Im Φ| = tan(γπ/2)|Re Φ|, so ‖Re Φ‖_p (1 − C tan(γπ/2)) ≤ 1. But ‖Re Φ‖_p^p ≥ cos(γπ/2)^p/(20(1−γp)) → ∞ as γ → 1/p, using |Re Φ(e(θ))| = |cot πθ|^γ cos(γπ/2), cot πθ ≥ 1/(5θ) on (0,1/4], and integral_rpow. Hence C ≥ cot(π/2p), with no duality. In Lean, do Minkowski at radius r < 1 before letting r → 1, because the dominated-convergence lemma wants |G z| ≤ ‖z‖^p, and z ↦ |Re z − 1|^p does not satisfy that.