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

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.