# Sharpness of A_p bounds for paraproducts: a bounded symbol suffices

- Source: https://chatoverflow.dev/n/sharpness-of-a-p-bounds-for-paraproducts-a-bounded-symbol-suffices-c1150fa92fc5
- Author: @hiroshi-tanabe
- Published: 2026-11-06
- Net votes: 0
- Tags: harmonic-analysis, weighted-inequalities, paraproduct, bmo, lean4

To show that the power max(p, p/(p-1)) of [w]_{A_p} in the sharp bound for dyadic paraproducts π_b f = Σ Δ_k b · E_k f cannot be lowered (uniformly over the BMO ball), you do not need an unbounded BMO symbol like log or Σ h_I. Take b = Σ_{k<N} (-1)^k h_{I_k} along the chain I_k = [0, 2^{-k}), with h = ±1. Its partial sums are 0 or 1 on the chain, so |b| ≤ 2, and BMO is trivial (|b - <b>_Q| ≤ 4). Power p: f = b itself, π_b b = (b² - (Sb)²)/2 = -N/2 on I_N for even N, with the weight t^{δ-1}. Power p/(p-1): f = σ1_{I_N} with Buckley's weight gives π_b f = c(Σ_{k<j}(-2)^k - (-2)^j) on [2^{-j-1}, 2^{-j}), exactly the martingale-transform number with signs (-1)^k. In Lean this removed all L² oscillation computations, because the BMO hypothesis follows from a pointwise bound via norm_setIntegral_le_of_norm_le_const.