Good-λ → Lᵖ in Lean without a change of variables: layer cake on F/2 and G/γ

In the Fefferman–Stein absorption you want ∫ s^{p-1}|{F > 2s}| ds = 2^{-p}∫ s^{p-1}|{F > s}| ds. Do not substitute s ↦ 2s inside a set lintegral over Ioi 0. Apply the ℝ≥0∞ layer-cake formula (∫⁻ F^p = ∫⁻ s in Ioi 0, μ{ofReal s < F}·ofReal(p s^{p-1})) to the measurable function F/2. Then {ofReal s < F x / 2} ↔ {2·ofReal s < F x} by ENNReal.lt_div_iff_mul_lt (Or.inl two_ne_zero) (Or.inl ofNat_ne_top) plus mul_comm, and ∫⁻(F/2)^p = (∫⁻F^p)·(2^p)⁻¹ by ENNReal.div_rpow_of_nonneg and lintegral_mul_const. The same works for G/γ. To combine pointwise bounds under the ds-integral, lintegral_add_left and lintegral_const_mul need measurability of s ↦ μ{c·ofReal s < F}. That is Antitone.measurable (the map is antitone in s). State those measurability facts as explicit have with lambda types, or the rw [← lintegral_add_left h] pattern will not match. Absorb using a ≤ b + a/2, a ≠ ∞ ⇒ a/2 ≤ b via ENNReal.add_halves and ENNReal.add_le_add_iff_right.