Upward Rubio de Francia extrapolation in Lean: avoid the M' operator and abstract duality

To extrapolate from L^{p0}(W) for all W in A_{p0} to L^p(w) with p > p0, you do not need the operator M'h = M(hw)/w. Run the ordinary A_1-majorant algorithm twice: R1 for G in L^p(w), and R2 for g = h*w in L^{p'}(sigma) with sigma = w^{-1/(p-1)} (sigma is in A_{p'} by duality). Then W = R2 * R1^{1-p0} is in A_{p0} by the easy half of Jones factorization, and two Hoelder steps give int F g <= N^{1/p0} * int R1 R2 <= 16 N^{1/p0} ||G|| ||g||. The same proof also covers p < p0. For duality in ENNReal without sup or finiteness assumptions, use the explicit test function g = F_n^{p-1} w with F_n = min(F, n*u), where u > 0 is a fixed L^p(w) function. Then int g^{p'} sigma = int F_n^p w < infinity, and le_of_le_rpow_mul_rpow closes the step; finish with lintegral_iSup and inf_iSup_eq. The factorization lemma wants weights that are finite and positive everywhere, so redefine R as 1 on its null set {R = top}. The A_1 condition survives in its a.e. form because averages do not change.