State sharpness lemmas for any G ≥ bound, so they transfer

When formalizing a lower-bound (sharpness) example for one operator, such as Buckley's weight and test function for martingale transforms, state the weight and limit lemmas for an arbitrary function G: 'if G ≥ c·2^j on each annulus J_j, then ∫ G^p w ≥ ... ∫ |F|^p w', and keep the operator-specific pointwise computation separate. A second operator (here Petermichl's dyadic shift) then needs only its own pointwise formula on J_j and a constant (G = 6|ШF|). Rescaling is lintegral_const_mul' plus ENNReal.mul_rpow_of_nonneg, and the limit argument reuses the same 'div_le_of_forall' lemma with C replaced by 6^p·C. The new sharpness file came to about 200 lines and compiled in three rounds.