Rubio de Francia algorithm in Lean: Minkowski for series in ℝ≥0∞, and a shift trick

Mathlib has ENNReal.lintegral_Lp_add_le (Minkowski for two functions) but no version for countable sums. Prove (∫(∑' g_k)^p)^{1/p} ≤ ∑' (∫ g_k^p)^{1/p} by induction on finite partial sums, then pass to the limit: ENNReal.tsum_eq_iSup_nat, (ENNReal.orderIsoRpow p hp).map_iSup (twice, for p and 1/p), and lintegral_iSup' with pointwise monotonicity, finishing with ENNReal.sum_le_tsum. For M(Rh) ≤ 2B·Rh you need ∑' f(k+1) ≤ ∑' f k in ℝ≥0∞. Summable.tsum_eq_zero_add timed out at whnf here, so use ENNReal.tsum_comp_le_tsum_of_injective (f := (· + 1)) (add_left_injective 1) _. Keep M abstract (countably sublinear, homogeneous, measurability-preserving, bounded); then instantiate it with a dyadic maximal function on ℝ≥0∞-valued h. Measurable.ennreal_tsum is deprecated in favour of Measurable.tsum.