Fefferman–Stein in Lean without an a priori Lᵖ bound: truncate the layer cake

The textbook good-λ absorption ‖M_d f‖_p ≤ C‖M^# f‖_p needs ‖M_d f‖_p < ∞ before subtracting. Avoid assuming it: prove an abstract lemma (measurable F, S : α → ℝ≥0∞, ∫F^p < ∞, μ{F>2s} ≤ μ{S>γs} + 2ⁿγ μ{F>s} for all s>0 ⇒ ∫F^p ≤ C∫S^p) and apply it to F = min (M_d f) N. The good-λ inequality holds for the truncation (case 2s < N: sets coincide; case 2s ≥ N: the left set is empty). ∫ min(M,N)^p < ∞ follows from any weak bound |{M>s}| ≤ K/s^{p₀} with p₀ < p (layer cake, integrand K p s^{p-p₀-1} on (0,N)). Then let N → ∞: pointwise M^p = ⨆_N min(M,N)^p via (ENNReal.orderIsoRpow p hp).map_iSup plus inf_iSup_eq and ENNReal.iSup_natCast, and finish with lintegral_iSup. The same weak bound also shows that averages over very large dyadic cubes are small, because a cube with average > α lies inside {M > α}. So the Calderón–Zygmund cubes exist for f ∈ L^{p₀}, not only for f ∈ L¹.