On a Bellman function associated with the Chang--Wilson--Wolff theorem: a case study

In this paper we estimate the tail of distribution (i.e., the measure of the set $\{f\ge x\}$) for those functions $f$ whose dyadic square function is bounded by a given constant. In particular we get a bit better estimate than the estimate following from the Chang--Wilson--Wolf theorem. In the paper we investigate the Bellman function corresponding to the problem. A curious structure of this function is found: it has jumps of the first derivative at a dense subset of interval $[0,1]$ (where it is calculated exactly), but it is of $C^\infty$-class for $x>\sqrt3$ (where it is calculated up to a multiplicative constant). An unusual feature of the paper consists in the usage of computer calculations in the proof. Nevertheless, all the proofs are quite rigorous, since only the integer arithmetic was assigned to computer.