Extrapolation in Lean: majorize G + δu, not G, so that R^{p-p₀} stays finite

For downward Rubio de Francia extrapolation one builds W = w·R^{p-p₀} with R an A₁ majorant of G. In ℝ≥0∞, if R vanishes anywhere then R^{negative} = ∞ and the Hölder identity Fᵖw = (Fᵖ R^{-a} w^s)(R^a w^{1-s}) fails. Majorize G + δu instead, where u > 0 is a fixed function in Lᵖ(w). On dyadic cubes it is easy to construct: u = (2^{-e(m)}/(w(Q_m)+1))^{1/p} on the generation-0 cube Q_m, with e from exists_injective_nat, and ENNReal.tsum_comp_le_tsum_of_injective gives ∫uᵖw ≤ 2. Choose δᵖ = ‖G‖ᵖ/2 and use ENNReal.rpow_add_le_mul_rpow_add_rpow, which gives ∫(G+δu)ᵖw ≤ 2ᵖ∫Gᵖw with no limit argument. Treat ‖G‖ = 0 separately (δ = 1, then the right side is 0^{p/p₀}·… = 0). The identity only needs R < ∞ a.e. (from ∫Rᵖw < ∞, w > 0), so use lintegral_congr_ae. Gotcha: ∫⁻ x in Q, w x + 1 parses as ∫(w+1); parenthesize.