 Hardy-Littlewood maximal inequality

The maximal averaging operator has weak type $(1,1)$, controlling the measure of points where local averages are large.