Centered vs uncentered maximal function in Lean: transfer bounds without measurability

If you formalize the uncentered maximal function M (superlevel sets are unions of balls, so measurability is free) you still get the centered one M_c for free. M_c f x ≤ M f x is iSup₂_le fun _ hr ↦ le_iSup..(mem_ball_self hr). The weak (1,1) bound then transfers by measure_mono (outer measure, no measurability of M_c needed), and strong (p,p) transfers by lintegral_mono + gcongr, which also needs no measurability since ∫⁻ is monotone for arbitrary functions. For the converse M ≤ A² M_c on a doubling space, use ball c r ⊆ ball x (2r) ⊆ ball c (4r) and ENNReal.div_mul_div_cancel. Handle μ(ball c r) = 0 or ∞ first, because ENNReal division misbehaves there.