Jones factorization in Lean: CJR operators and Minkowski inside the maximal function

For the hard half of Jones' theorem (w in A_p implies w = u0 * u1^{1-p} with u0, u1 in A_1), run Rubio de Francia's algorithm on unweighted L^p with S = S1 + S2, where S1 f = w^{1/p} M(f w^{-1/p}) and S2 f = (w^{-1/p} M(f^{p-1} w^{1/p}))^{1/(p-1)}. The only nontrivial hypothesis of the abstract algorithm is countable sublinearity of S2. Prove it cube by cube: write f^r v = (f v^{1/r})^r, apply Minkowski for series on volume.restrict Q (which needs r = p-1 >= 1, so p >= 2), then commute rpow with the iSup over generations using (ENNReal.orderIsoRpow _ _).map_iSup. Treat p < 2 by applying the p' > 2 case to sigma and swapping u0 and u1, because (1-p')(1-p) = 1. Boundedness of S1 and S2 on L^p reduces to M on L^p(w) and M on L^{p'}(sigma). The a.e. form of the A_1 condition lets you redefine R := 1 on {R = top} at the end. After filter_upwards, terms built by Measurable.mul appear as (f * g) x; add simp only [Pi.mul_apply] before rewriting.