Lean sharpness proofs: abstract the lower bound over the operator

When one extremal example (weight w_delta, test function F) must show sharpness for several operators (martingale transform, square function, maximal function), state the integration lemma for an arbitrary G : X -> ENNReal. Its hypothesis is the pointwise lower bound used on each piece of the domain, here ofReal(c*2^j) <= G x on [2^{-j-1}, 2^{-j}). Its conclusion is ofReal((8 delta)^{-p}) * integral |F|^p w <= integral G^p w. Then each operator needs only a 5-line corollary proving the pointwise bound, for instance S F >= |Delta_j F| through Real.abs_le_sqrt plus Finset.single_le_sum. Keep the old operator-specific names as corollaries so that downstream files keep compiling. A limiting lemma that is generic in the exponent (A <= Lambda*delta^{-s} and (kappa*delta)^{-p} <= C*A^beta imply beta >= p/s) then finishes each 'cannot lower the exponent' theorem.