Periodicity follows directly from the definitions. The other properties are part of the Lean library.

Let N_0 be as in Lemma 1.11.1.2. For every x\in [0,2\pi)\setminus E and every N>N_0 we have by the triangle inequality |f(x)-S_N f(x)| \le |f(x)-f_0(x)|+|f_0(x)-S_N f_0(x)|+|S_N f_0(x)-S_N f(x)|. Using Lemma 1.11.1.1, Lemma 1.11.1.2, and Lemma 1.11.1.3, the right-hand side is bounded by \epsilon' + \frac\epsilon4 + \frac\epsilon4 \le \epsilon. This shows the desired estimate for the given E and N_0.

Proof of Theorem 1.1.1. By applying Theorem 1.11.1.4 with a sequence of \epsilon_n := 2^{-n}\delta for n\ge 1 and taking the union of corresponding exceptional sets E_n, we see that outside a set of measure \delta, the partial Fourier sums converge pointwise for N\to \infty. Applying this with a sequence of \delta shrinking to zero and taking the intersection of the corresponding exceptional sets, which has measure zero, we see that the Fourier series converges outside a set of measure zero.

By definitions and interchanging sum and integral, S_Nf(x)=\sum_{n=-N}^N \widehat f_n e^{inx} =\sum_{n=-N}^N\frac{1}{2\pi}\int_0^{2\pi} f(y)e^{in(x-y)}\,dy. Thus S_Nf(x)=\frac{1}{2\pi}\int_0^{2\pi} f(y)\sum_{n=-N}^Ne^{in(x-y)}\,dy. This proves the first statement of the lemma. By a telescoping sum, for every x'\in\mathbb{R} we have \left(e^{\frac12 ix'}-e^{-\frac12 ix'}\right) \sum_{n=-N}^Ne^{inx'} = e^{(N+\frac12)ix'}-e^{-(N+\frac12)ix'}. If e^{ix'}\ne 1, the first factor on the left-hand side is not zero and we may divide by it to obtain \sum_{n=-N}^Ne^{inx'} =\frac{e^{i(N+\frac12)x'}}{e^{\frac12 ix'}-e^{-\frac12 ix'}} -\frac{e^{-i(N+\frac12)x'}}{e^{\frac12 ix'}-e^{-\frac12 ix'}} =\frac{e^{iNx'}}{1-e^{-ix'}} +\frac{e^{-iNx'}}{1-e^{ix'}}. This proves the second part of the lemma.

We have |1-e^{ix}|=\sqrt{(1-\cos x)^2+\sin^2x}\ge |\sin x|. For 0\le x\le \pi/2, concavity of \sin on [0,\pi], together with \sin(0)=0 and \sin(\pi/2)=1, gives |\sin x|\ge \frac{2}{\pi}x\ge \frac{2}{\pi}\eta. The remaining intervals x\in \frac{m\pi}{2}+[0,\frac{\pi}{2}] for m\in\{-4,-3,-2,-1,1,2,3\} are handled similarly.

Fix x\ne y. If \kappa(x-y)=0, the estimate is immediate. Otherwise 0<|x-y|<1, and |\kappa(x-y)|= \left|\frac{1-|x-y|}{1-e^{i(x-y)}}\right|. Using Lemma 1.11.1.9, |\kappa(x-y)|\le \frac{1}{|1-e^{i(x-y)}|} \le \frac{2}{|x-y|}, which proves the stated bound.

Upon replacing y by y-x and y' by y'-x in the left-hand side of the closeness assumption, we can assume that x=0. Then the assumption implies that y and y' have the same sign. Since \kappa(y)=\bar\kappa(-y), we can assume that they are both positive, and then it follows that \frac{y}{2}\le y'. We distinguish four cases.

If y,y'\le 1, then |\kappa(-y)-\kappa(-y')| =\left|\frac{1-y}{1-e^{-iy}}-\frac{1-y'}{1-e^{-iy'}}\right| and by the fundamental theorem of calculus this equals \left|\int_{y'}^y \frac{-1+e^{-it}+i(1-t)e^{it}}{(1-e^{-it})^2}\,dt\right|. Using y'\ge y/2 and Lemma 1.11.1.9, we bound this by \le |y-y'|\sup_{\frac{y}{2}\le t\le 1}\frac{3}{|1-e^{-it}|^2} \le 3|y-y'|\left(2\frac{2}{y}\right)^2 \le 2^6\frac{|y-y'|}{|y|^2}. If y\le 1 and y'>1, then \kappa(-y')=0 and the first case gives |\kappa(-y)-\kappa(-y')| =|\kappa(-y)-\kappa(-1)| \le 2^6\frac{|y-1|}{|y|^2} \le 2^6\frac{|y-y'|}{|y|^2}. Similarly, if y>1 and y'\le 1, then \kappa(-y)=0 and the first case gives |\kappa(-y)-\kappa(-y')| =|\kappa(-y')-\kappa(-1)| \le 2^6\frac{|y'-1|}{|y'|^2} \le 2^6\frac{|y-y'|}{|y'|^2}. Using again y'\ge y/2, this is bounded by \le 2^6\frac{|y-y'|}{|y/2|^2} =2^8\frac{|y-y'|}{|y|^2}. Finally, if y,y'>1, then |\kappa(-y)-\kappa(-y')|=0 \le 2^8\frac{|y-y'|}{|y|^2}.

This is part of the Lean library.

This is part of the Lean library.

By Lemma 1.11.2.2, it suffices to show that the Fourier coefficients \widehat{f}_n are summable. Applying Lemma 1.11.2.1 twice and using the fact that f'' is continuous and therefore bounded on [0,2\pi], we compute \sum_{n\in \mathbb{Z}} |\widehat{f}_n| = |\widehat{f}_0| + \sum_{n\in \mathbb{Z}\setminus \{0\}} \frac {1}{n^2} |\widehat{f''}_n| \le |\widehat{f}_0| + \left(\sup_{x\in [0,2\pi]} |f(x)| \right) \cdot \sum_{n\in \mathbb{Z}\setminus \{0\}} \frac {1}{n^2}<\infty.

Lemma 1.11.1.2 now follows directly from Lemma 1.11.2.3.

We have \|M_ng\|_{L^2[0,2\pi]}^2 =\int_0^{2\pi}|e^{inx}g(x)|^2\,dx =\int_0^{2\pi}|g(x)|^2\,dx =\|g\|_{L^2[0,2\pi]}^2. By the triangle inequality, the square root of this identity, and Lemma 1.11.1.10, \|L_Ng\|_{L^2[0,2\pi]} =\left\|\frac1N\sum_{n=0}^{N-1} M_{n+N}S_{N+n}M_{-N-n}g\right\|_{L^2[0,2\pi]} \le \frac1N\sum_{n=0}^{N-1} \|M_{n+N}S_{N+n}M_{-N-n}g\|_{L^2[0,2\pi]} = \frac1N\sum_{n=0}^{N-1} \|S_{N+n}M_{-N-n}g\|_{L^2[0,2\pi]} \le \frac1N\sum_{n=0}^{N-1}\|M_{-N-n}g\|_{L^2[0,2\pi]} =\|g\|_{L^2[0,2\pi]}.

By periodicity and change of variables, \int_{-x}^0 f(y)\,dy =\int_{-x}^0 f(y+2\pi)\,dy =\int_{2\pi-x}^{2\pi} f(y)\,dy. Breaking up the domain of integration and using this identity gives \int_0^{2\pi}f(y)\,dy =\int_0^{2\pi-x}f(y)\,dy+\int_{2\pi-x}^{2\pi}f(y)\,dy =\int_0^{2\pi-x}f(y)\,dy+\int_{-x}^0f(y)\,dy =\int_{-x}^{2\pi-x}f(y)\,dy. The second identity follows by substituting y by y-x.

Using Fubini and Lemma 1.11.3.2, we have \int_0^{2\pi}\int_0^{2\pi}f(y)^2g(x-y)\,dy\,dx =\int_0^{2\pi}f(y)^2\int_0^{2\pi}g(x-y)\,dx\,dy =\int_0^{2\pi}f(y)^2\int_0^{2\pi}g(x)\,dx\,dy =\|f\|_{L^2[0,2\pi]}^2\|g\|_{L^1[0,2\pi]}. Let h be the nonnegative square root of g; then h is bounded and 2\pi-periodic with h^2=g. By Cauchy--Schwarz and the preceding identity, the square of the left-hand side is at most \int_0^{2\pi}\left(\int_0^{2\pi}f(y)^2g(x-y)\,dy\right) \left(\int_0^{2\pi}g(x-y)\,dy\right)\,dx =\|f\|_{L^2[0,2\pi]}^2\|g\|_{L^1[0,2\pi]}^2. Taking square roots proves the lemma.

By monotonicity of the integral and the pointwise bound on g, \|g\|_{L^1[0,2\pi]}\le \int_0^{2\pi}k_r(x)\,dx. Using the symmetry k_r(x)=k_r(-x), the assumption, and Lemma 1.11.1.9, the last display is 2\int_0^\pi \min\left(\frac1r,1+\frac{r}{|1-e^{ix}|^2}\right)\,dx \le 2\int_0^r\frac1r\,dx +2\int_r^\pi\left(1+\frac{64r}{x^2}\right)\,dx \le 2+2\pi+2\left(\frac{4r}{r}-\frac{4r}{\pi}\right)\le 17. Together with Lemma 1.11.3.3, this proves the lemma.

By definition and Lemma 1.11.1.8, L_Ng(x)=\frac1N\sum_{n=0}^{N-1} \int_0^{2\pi}e^{-i(N+n)x}K_{N+n}(x-y)e^{i(N+n)y}g(y)\,dy. This has the required convolution form with L'(x)=\frac1N\sum_{n=0}^{N-1}K_{N+n}(x)e^{-i(N+n)x}. With the exponential-sum formula eqksumexp from Lemma 1.11.1.8, we have |K_N(x)|\le 2N+1 for every x, and hence |L'(x)|\le \frac1N\sum_{n=0}^{N-1}(2N+2n+1)\le 4N\le 2^3r^{-1}. Therefore, for |x|\in [0,r)\cup(1,\pi], we have \left|L'(x)-\mathbf{1}_{\{y:\,r<|y|<1\}}(x)\kappa(x)\right| =|L'(x)|\le 2^3r^{-1}. This proves eqdifflhil for |x|\in[0,r) since k_r(x)=r^{-1} in this case.

For e^{ix}\ne 1, the Hilbert-form expression eqksumhil from Lemma 1.11.1.8 gives L'(x)=\frac1N\sum_{n=0}^{N-1} \left(\frac{e^{i(N+n)x}}{1-e^{-ix}}+ \frac{e^{-i(N+n)x}}{1-e^{ix}}\right)e^{i(N+n)x} =\frac1N\sum_{n=0}^{N-1} \left(\frac{e^{i2(N+n)x}}{1-e^{-ix}}+\frac1{1-e^{ix}}\right) and hence L'(x)=\frac{1}{1-e^{ix}} +\frac1N\frac{e^{i2Nx}}{1-e^{-ix}}\sum_{n=0}^{N-1}e^{i2nx}. Therefore L'(x)-\mathbf{1}_{\{y:\,r<|y|<1\}}\kappa(x) =L''(x)+ \frac{1-\mathbf{1}_{\{y:\,r<|y|<1\}}(x)(1-|x|)}{1-e^{ix}}, where L''(x):=\frac1N\frac{e^{i2Nx}}{1-e^{-ix}}\sum_{n=0}^{N-1}e^{i2nx}. For x\in[-\pi,r]\cup[r,\pi], using Lemma 1.11.1.9 gives \left|\frac{1-\mathbf{1}_{\{y:\,r<|y|<1\}}(x)(1-|x|)}{1-e^{ix}}\right| =\left|\frac{\min(|x|,1)}{1-e^{ix}}\right| \le \frac{2\min(|x|,1)}{|x|} \le 2k_r(x).

It remains to estimate L''. If the real part of e^{ix} is negative, then 1\le |1-e^{-ix}|\le 2, so |L''(x)|\le \frac1N\sum_{n=0}^{N-1}1=1 \le 1+\frac{r}{|1-e^{ix}|^2}. If the real part is positive and still e^{ix}\ne\pm1, telescoping gives (1-e^{2ix})\sum_{n=0}^{N-1}e^{i2nx}=1-e^{i2Nx}. As e^{2ix}\ne1, we may divide by 1-e^{2ix} and insert this into eqhil3 to obtain L''(x)=\frac1N\frac{e^{i2Nx}}{1-e^{-ix}} \frac{1-e^{i2Nx}}{1-e^{2ix}}, and, using the nonnegativity of the real part of e^{ix}, |L''(x)|\le \frac2N\frac1{|1-e^{ix}|}\frac1{|1-e^{2ix}|} =\frac2N\frac1{|1-e^{ix}|^2}\frac1{|1+e^{ix}|} \le \frac{2r}{|1-e^{ix}|^2} \le 2\left(1+\frac{r}{|1-e^{ix}|^2}\right). For |x|\in [r,\pi], one checks 1+\frac{r}{|1-e^{ix}|^2}\le 5k_r(x). Thus the estimates above show that |L''(x)|\le 10k_r(x) in this range. Together with the previous 2k_r(x) bound, this proves eqdifflhil for |x|\in[r,\pi]. Since |x|\in[0,r) was covered by eqdiffzero, this completes the proof.

Proof of Lemma 1.11.1.6. We first show that if f is supported in [1,4], then \|H_rf\|_{L^2[2,3]}\le 2^8\|f\|_{L^2(\mathbb{R})}. Let \tilde f be the 2\pi-periodic extension of f to \mathbb{R}, and let N be the smallest integer larger than 1/r. Then the identity eqdifflhil shows that the kernels of H_r and 2\pi L_N differ by at most 12k_r on [-\pi,\pi]. Consider x\in[2,3]. When computing H_rf(x) and 2\pi L_Nf(x), the kernels are computed at points of the form x-y with f(y)\ne0, hence y\in[1,4]. Since x\in[2,3], the difference x-y is bounded in absolute value by 2 and therefore belongs to [-\pi,\pi], where the above bound holds.

Thus for x\in[2,3], |H_r\tilde f(x)|\le 2\pi |L_N\tilde f(x)| +12\left|\int_0^{2\pi}k_r(x-y)\tilde f(y)\,dy\right|. Taking the L^2 norm and using subadditivity gives \|H_r\tilde f\|_{L^2[2,3]}\le 2\pi\|L_N\tilde f\|_{L^2[0,2\pi]} +12\left(\int_0^{2\pi} \left|\int_0^{2\pi}k_r(x-y)\tilde f(y)\,dy\right|^2\,dx\right)^{1/2}. Since \kappa is supported in [-1,1], H_r\tilde f agrees with H_rf on [2,3]. Using Lemma 1.11.3.1 and Lemma 1.11.3.4, gives \|H_rf\|_{L^2[2,3]} \le 2\pi\|f\|_{L^2[0,2\pi]}+12\cdot 17\|f\|_{L^2[0,2\pi]}, which gives the short-support estimate.

Suppose now that f is supported in [c,c+3] for some c\in\mathbb{R}. Then g(x)=f(x-c+1) is supported in [1,4]. By a change of variables in def-H-r, H_rg(x)=H_rf(x-c+1). Thus, by the short-support estimate, \|H_rf\|_{L^2[c+1,c+2]}\le 2^8\|f\|_2. Let now f be arbitrary. Since \kappa(x)=0 for |x|>1, for all x\in[c+1,c+2] we have H_rf(x)=H_r(f\mathbf{1}_{[c,c+3]})(x). Thus \int_{c+1}^{c+2}|H_rf(x)|^2\,dx =\int_{c+1}^{c+2}|H_r(f\mathbf{1}_{[c,c+3]})(x)|^2\,dx. Applying the short-support bound gives \le 2^{16}\int_c^{c+3}|f(x)|^2\,dx. Summing over all c\in\mathbb{Z} gives \int_{\mathbb{R}}|H_rf(x)|^2\,dx \le 3\cdot 2^{16}\int_{\mathbb{R}}|f(x)|^2\,dx. This completes the proof.

Proof of Lemma 1.11.1.7. Let g be Lipschitz continuous as in the lemma. If n=0, then \int_\alpha^\beta g(x)\,dx \le |\beta-\alpha|\sup_{\alpha\le x\le\beta}|g(x)| \le |\beta-\alpha|\|g\|_{\operatorname{Lip}(\alpha,\beta)} (1+|n||\beta-\alpha|)^{-1}. Assume now n\ne 0; by symmetry we may suppose n>0.

If \beta-\alpha<\pi/n, the triangle inequality gives \left|\int_\alpha^\beta g(x)e^{inx}\,dx\right| \le |\beta-\alpha|\sup_{x\in[\alpha,\beta]}|g(x)| \le 2\pi|\beta-\alpha|\|g\|_{\operatorname{Lip}(\alpha,\beta)} (1+|n||\beta-\alpha|)^{-1}. Now suppose \pi/n\le \beta-\alpha. Since e^{in(x+\pi/n)}=-e^{inx}, we write \int_\alpha^\beta g(x)e^{inx}\,dx =\frac12\int_\alpha^\beta g(x)e^{inx}\,dx -\frac12\int_\alpha^\beta g(x)e^{in(x+\pi/n)}\,dx. We split the first integral at \alpha+\pi/n and the second one at \beta-\pi/n, and make a change of variables in the second part of the first integral to obtain =\frac12\int_\alpha^{\alpha+\pi/n}g(x)e^{inx}\,dx -\frac12\int_{\beta-\pi/n}^{\beta}g(x)e^{in(x+\pi/n)}\,dx +\frac12\int_{\alpha+\pi/n}^{\beta} \left(g(x)-g\left(x-\frac{\pi}{n}\right)\right)e^{inx}\,dx. The sum of the first two terms is, by the triangle inequality, bounded by \frac{\pi}{n}\sup_{x\in[\alpha,\beta]}|g(x)|. The third term is, by the triangle inequality, at most \frac12\int_{\alpha+\pi/n}^{\beta} \left|g(x)-g\left(x-\frac{\pi}{n}\right)\right|\,dx \le \frac{|\beta-\alpha|}{2}\frac{\pi}{n} \sup_{\alpha\le x<y\le\beta}\frac{|g(x)-g(y)|}{|x-y|}. Adding the two terms, we obtain \left|\int_\alpha^\beta g(x)e^{-inx}\,dx\right| \le \frac{\pi}{n}\|g\|_{\operatorname{Lip}(\alpha,\beta)}. This completes the proof of the lemma, using that with \frac{\pi}{n}\le \beta-\alpha, \frac{\pi}{n} =\frac{2\pi|\beta-\alpha|}{2n|\beta-\alpha|} \le 2\pi|\beta-\alpha|(1+n|\beta-\alpha|)^{-1}, as required.

Proof of Lemma 1.11.1.10. The functions e_n:x\mapsto e^{inx} form an orthonormal basis in L^2[-\pi,\pi], which is already in Mathlib. Therefore \|S_Nf\|^2_{L^2[-\pi,\pi]} =\left\|\sum_{n=-N}^N \langle\widehat f_n,e_n\rangle_{L^2[-\pi,\pi]}\right\|^2_{L^2[-\pi,\pi]} =\sum_{n=-N}^N|\widehat f_n| \le \sum_{n\in\mathbb{Z}}|\widehat f_n| =\|f\|_{L^2[-\pi,\pi]}. This completes the proof.