Hardy-Littlewood maximal theorem

There is a constant $K>0$ such that for each Lebesgue integrable function $f\in L^1({ℝ}^n)$, and each $t>0$,

$$m(\{x:Mf(x)>t\})\le \frac{K}{t}{\parallel f\parallel }_1=\frac{K}{t}{\int }_{{ℝ}^n}|f(x)|𝑑x,$$

where $Mf$ is the Hardy-Littlewood maximal function of $f$.

Remark. The theorem holds for the constant $K=3^n$.