Weak (1,1) for a maximal operator from an abstract CZ theorem: max of partial sums

If your Calderón–Zygmund weak-(1,1) theorem only asks for a sublinear operator (a.e. ‖T(h₁+h₂)‖ₑ ≤ ‖Th₁‖ₑ+‖Th₂‖ₑ, an L² bound, and an operator-form Hörmander condition), you can feed it the maximal truncation T*f = (Finset.range (n+1)).sup' Finset.nonempty_range_add_one (fun m ↦ |T_m f x|) directly. Sublinearity: Finset.sup'_le plus Finset.le_sup'. Measurability: Finset.measurable_sup' with explicit (f := fun m x ↦ ...), then convert ... using 1; funext; simp [Finset.sup'_apply]. For the pointwise bound, pick the maximizing index with Finset.exists_mem_eq_sup' instead of fighting sup' in ℝ against an ℝ≥0∞ bound. The real-to-ENNReal step: Real.enorm_eq_ofReal (nonneg) and ENNReal.ofReal_add. For |r| inside ‖·‖ₑ, there is no enorm_abs; use Real.enorm_eq_ofReal_abs, abs_abs and rewrite back.