The maximal function of a function on the plane gives at each point the largest average of its absolute value over axis-parallel squares centred there. A covering argument bounds the area where it exceeds a level by 4 times the integral of the function's absolute value, divided by the level. The best possible factor is unknown. Lin proved in the Lean proof assistant that it is below 3.879, and reached 3.615749 with an auxiliary function combining a cut-off singular power and splines. A better function of that type, found here, gives 3.59123.
Abstract
Let c2 be the best constant in the weak type (1,1) inequality for the centred Hardy–Littlewood maximal operator over axis-parallel squares in the plane. The covering argument gives c2 ≤ 4, and Lin proved c2 < 3.879, with a proof formalized in Lean. We prove c2 ≤ 3.59123. The proof uses a comparison principle of Lin, in coordinates (u, v) in which squares become diamonds: if an even, nonnegative, integrable kernel K is at least 1 on the diamond |u| + |v| ≤ 1 and AαK ≥ 0 away from the origin, where Aα = −|∂u|α − |∂v|α and 0 < α < 2, then c2 is at most half the integral of K. We prove this principle in detail, following Lin, and give closed forms for Aα applied to cubic B-splines and to (|u| + |v|)−α. With these, AαK is explicit for kernels made of a truncation of (|u| + |v|)−α and finitely many tensor products of cubic B-splines. We exhibit such a kernel for α = 47/40 with B-spline spacing 1/32, and two independent programs verify its properties in interval arithmetic. This improves the bound c2 < 3.615749 that Lin obtained with a kernel of this type.
Illustration of the certified kernel K, the auxiliary function of the proof, in the coordinates (u, v) in which squares become diamonds. Left: K on a logarithmic scale, darker where it is larger, white below 0.003 and grey where it is 0. It tends to infinity at the centre, is at least 1 on the unit diamond |u| + |v| ≤ 1 (solid outline) and is nonnegative everywhere; its singular part vanishes outside the dashed diamond |u| + |v| = 33/20. Right: AK, where A integrates, along the horizontal and the vertical direction, the second differences of K over all step lengths t with weight |t|^(−1−α), α = 47/40; logarithmic scale, white below 2.5·10⁻⁴. Lin's comparison principle, which turns K into the bound, also needs AK ≥ 0 away from the centre. In this picture AK is exactly 0 only in the small grey corners, where neither the horizontal nor the vertical line through the point meets the support of K, which lies in the square max(|u|, |v|) ≤ 9/4. The yellow dots mark a local minimum of AK of about 2.8·10⁻⁴ and its copies under the symmetries of the square; this dip is far narrower than a pixel. Half the integral of K is 3.5912243…, so the best possible factor is at most 3.59123; the picture is computed in floating point from the certificate's exact data.
