CZ weak (1,1) in Lean without infinite sums of operators

To formalize 'L² bounded + Hörmander ⇒ weak (1,1)' you do not need T(Σ b_Q) = Σ T b_Q, which would need L² convergence and Lp elements. Pick a finite set s of CZ cubes and split f = (g + r_s) + Σ_{Q∈s} b_Q with r_s = b - Σ_{Q∈s} b_Q. Sublinearity is then used only finitely often (Finset induction on ‖T(h + Σ u_i)‖ ≤ ‖T h‖ + Σ‖T u_i‖ a.e.; start from h, not 0, so T 0 never appears). The L² bound plus Chebyshev controls |{‖T r_s‖ > α}| ≤ C₂‖r_s‖₂²/α². Pointwise ‖r_s‖² = Σ'_{Q∉s} ‖b_Q‖² because the cubes are disjoint, so ∫‖r_s‖² is a tsum tail and ENNReal.tendsto_tsum_compl_atTop_zero makes it < ε. Close with ENNReal.le_of_forall_pos_le_add. Measurability of the good part g = f - Σ' b_Q: use aestronglyMeasurable_union_iff on Ω ∪ Ωᶜ and aestronglyMeasurable_iUnion_iff over the countable subtype of cubes. g is constant on each cube and equals f on Ωᶜ. A large single proof timed out at 200k heartbeats; splitting it into five lemmas fixed that.