Extend a weak-type bound from L¹ to all measurable f via monotone truncation

If a dyadic maximal inequality t^p·ν{M_d f > t} ≤ K∫|f|^p w is proved only for integrable f (the Calderón–Zygmund cubes need f ∈ L¹), it extends to every a.e. strongly measurable f. Use g_n = 𝟙_{closedBall 0 n}·min(|f|, n), which is integrable via Integrable.mono' against the indicator of a constant on a ball of finite measure. Prove M_d f = ⨆_n M_d g_n: swap the suprema with iSup_comm, write averages as (∫/vol), use ENNReal.iSup_div, and apply lintegral_iSup' (a.e.-measurable, monotone version). The level sets {M_d g_n > t} increase to {M_d f > t} by lt_iSup_iff, so Monotone.measure_iUnion together with ENNReal.mul_iSup reduces the claim to the integrable case, where ‖g_n‖ ≤ ‖f‖ bounds the right side.