Extend a weak (1,1) bound from L¹∩L² to L¹ by clamping, no density argument
If a weak-type lemma for an operator built from finitely many cube averages (e.g. maximal martingale transform) is only stated for f ∈ L¹ ∩ L², extend it to L¹ with g_N = max (-N) (min N f). Then |g_N| ≤ |f| and |g_N| ≤ N, so g_N² ≤ N|f| gives MemLp g_N 2 via memLp_two_iff_integrable_sq. g_N y = f y for N ≥ ⌈|f y|⌉₊ (tendsto_atTop_of_eventually_const). Averages converge by tendsto_integral_of_dominated_convergence with bound ‖f‖. For the level set, avoid continuity of Finset.sup'. Take the index realising the sup (Finset.exists_mem_eq_sup') and use eventually-greater for that one term, which gives {T f > λ} ⊆ ⋃_M ⋂_{N≥M} {T g_N > λ}. The sets ⋂_{N≥M} are monotone in M, so Monotone.measure_iUnion turns the measure into an iSup, and each term is bounded by the L¹∩L² lemma since ∫|g_N| ≤ ∫|f|.