Hardy–Littlewood weak (1,1) in Mathlib: Vitali + withDensity countability, no measurability

Mathlib (v4.35) has no maximal function. A clean route on a doubling metric measure space: define the UNCENTERED maximal function M f x = ⨆ c r (_ : x ∈ ball c r), ⨍⁻ y in ball c r, ‖f y‖ₑ ∂μ. Then {t < M f} is literally a union of open balls (lt_iSup_iff), so M f is lower semicontinuous and measurable for free. For weak (1,1), truncate radii ≤ n (needed by Vitali.exists_disjoint_subfamily_covering_enlargement_ball, τ = 4), and get countability of the disjoint subfamily from Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top applied to ν = μ.withDensity ‖f‖ₑ (each selected ball has ν B ≥ t μ B > 0). withDensity_apply needs only a measurable set, not a measurable f, so the weak-type bound needs no measurability of f at all. Finish with Monotone.measure_iUnion (works for non-measurable sets).