Marcinkiewicz interpolation in Lean/Mathlib: proof layout that compiles

Working pattern (all in ℝ≥0∞, operator T : (α → E) → β → ℝ≥0∞, weak type stated as ν{t < T f} ≤ C * (∫⁻ ‖f‖ₑ^p₀) / t^p₀). (1) Prove an ℝ≥0∞ layer cake ∫⁻ F^p = ∫⁻ s in Ioi 0, ν{ofReal s < F} * ofReal(p s^(p-1)) by Tonelli on the 1-D identity ∫⁻ s in Ioi 0, {s | ofReal s < a}.indicator (ofReal(q s^(q-1))) = a^q (a may be ∞). (2) Prove two reusable Tonelli lemmas, head ∫₀^∞ s^(a-1) ∫_{c g > s} g^q = c^a/a ∫ g^(q+a) and tail ∫₀^∞ s^(-b-1) ∫_{c g ≤ s} g^q = c^(-b)/b ∫ g^(q-b) (needs b < q and g < ∞). Get product measurability by writing the integrand as Ψ(g x, s) with Ψ measurable on ℝ≥0∞ × ℝ and using hΨ.comp_aemeasurable (hg.comp_snd.prodMk measurable_fst.aemeasurable). (3) For f only AEStronglyMeasurable, split with S = {2‖f‖ > s}, using hf.indicator₀ (nullMeasurableSet_lt ..) and indicator_self_add_compl, and replace ‖f‖ₑ by the measurable G = ‖hf.mk f ·‖ₑ only inside integrals via lintegral_congr_ae. (4) Isolate the weight identity p s^(p-1)/(s/2)^r = p 2^r s^(p-r-1) as its own lemma.