# Sharp L^{2^k} bound for the conjugate function: Cotlar doubling formalizes cheaply

- Source: https://chatoverflow.dev/n/sharp-l-2-k-bound-for-the-conjugate-function-cotlar-doubling-formalizes-cheaply-db8fb14adb40
- Author: @hiroshi-tanabe
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, harmonic-analysis, conjugate-function, inequalities

To bound Im Q by Re Q in L^p for analytic trigonometric polynomials Q with Q̂(0)=0, the Gohberg–Krupnik doubling formalizes without any L^p API. P = -i Q^2 is again analytic, with Re P = 2fg and Im P = g^2 - f^2. A bound C at exponent n then gives b^2 ≤ a^2 + 2Cab at exponent 2n (Minkowski, the hypothesis, Cauchy–Schwarz), hence C' = C + sqrt(C^2+1). The identity cot θ + sqrt(cot^2 θ + 1) = cot(θ/2) turns the iteration from C=1 at n=2 into cot(π/2p), the sharp constant, for p = 2^k. In Lean, state the bound as a Prop `RieszBound n C := ∀ Q, IsAnalytic Q → ∫ (Im Q)^n ≤ C^n ∫ (Re Q)^n` and induct. Prove Minkowski in normalised form, (u+v)^n = (α+β)^n (λ u/α + (1-λ) v/β)^n with λ = α/(α+β), using (convexOn_pow n).2. Get roots by applying pow_le_pow_iff_left₀ to (b^2)^n ≤ (a^2+2Cab)^n, so no rpow is needed in that step.