Sharp upward extrapolation: majorize only the dual function, W = w^θ V^{1-θ}

To extrapolate ∫F^{p0}W ≤ N∫G^{p0}W from p0 to p > p0 with the sharp threshold [W]_{A_{p0}} ≲ [w]_{A_p} (Duoandikoetxea), do not use the two-majorant weight W = R2·R1^{1-p0}. That weight gives [w]^{1+(p0-1)/(p-1)}. Instead take θ = (p0-1)/(p-1), truncate F_n = min(F, n u), and let V be a Rubio de Francia majorant of φ = F_n^{p-1} w in L^{p'}(σ). Then W = w^θ V^{1-θ} satisfies [W]_{A_{p0}} ≤ [w]_{A_p}^θ [V]_{A_1}^{1-θ} (Hölder for ⨍W; the dual weight is σ·V^{-(1-θ)/(p0-1)}, bounded using V ≥ ⨍V/C). Moreover [V]_{A_1} ≲ ‖M‖_{L^{p'}(σ)} ≲ [w]_{A_p} by Buckley. Two identities close the argument: (p-1)(1-θ) = p-p0 gives F_n^{p-p0} w ≤ W, and Hölder with exponents (p/p0, p/(p-p0)) on G^{p0}w^{p0/p}·V^{1-θ}w^{θ-p0/p} gives exactly ∫G^p w and ∫V^{p'}σ. G needs no majorant, so the cases ∫G^p w = 0 or ∞ need no special treatment. In Lean the A_1 hypothesis can be a.e. (∀ᵐ y, y ∈ Q → ⨍_Q V ≤ C V y); finiteness of ⨍_Q V then follows from V < ∞ everywhere.