Fejér kernel and Fejér's theorem

DefinitionThe Fejér kernel#✓fully proved

Let \(T > 0\) and, for \(n \in \mathbb{Z}\), let \(e_n(x) = e^{2\pi i n x / T}\) be the \(n\)-th Fourier character on the circle \(\mathbb{R}/T\mathbb{Z}\). For a natural number \(N\), the \(N\)-th Fejér kernel is the function \(K_N : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\) given by the Cesàro mean of the Dirichlet kernels, \(K_N(x) = \frac{1}{N+1} \sum_{k=0}^{N} \sum_{n=-k}^{k} e_n(x)\).

Writing \(x\) also for a real representative, when \(\sin(\pi x / T) \ne 0\) the kernel has the closed form \(K_N(x) = \frac{1}{N+1} \left(\frac{\sin((N+1)\pi x / T)}{\sin(\pi x / T)}\right)^2\). This normalization is for the Haar probability measure on \(\mathbb{R}/T\mathbb{Z}\); for \(T = 2\pi\), the kernel for integration against Lebesgue measure is \(K_N / (2\pi)\).

noncomputable def fejerKernel (N : ℕ) : AddCircle T → ℂ :=
  fun x => ((N : ℂ) + 1)⁻¹ • ∑ k ∈ range (N + 1),
    ∑ n ∈ Finset.Icc (-(k : ℤ)) (k : ℤ), fourier n x

Used by 11

Used byCesàro–Fourier means are convolutions with the Fejér kernel · Quantitative Fejér theorem · Continuity of the Fejér kernel · The Fejér kernel as a squared modulus · Integrability of the Fejér kernel · Nonnegativity of the Fejér kernel · Properties of the Fejér kernel · Symmetry of the Fejér kernel · The Fejér kernel has integral one · The Fejér kernel has \(L^1\) norm one · Pointwise bound for the Fejér kernel

TheoremIntegrability of Fourier characters#✓fully proved

Let \(T > 0\). For every integer \(n\), the Fourier character \(e_n(x) = e^{2\pi i n x / T}\) is integrable on the circle \(\mathbb{R}/T\mathbb{Z}\) with respect to the normalized Haar measure, the Haar measure of total mass \(1\).

theorem fourier_integrable (n : ℤ) :
    Integrable (fun t : AddCircle T => (fourier n t : ℂ)) haarAddCircle

Used by 2

Used byThe Dirichlet kernel has integral one · The Fejér kernel has integral one

TheoremIntegral of a Fourier character#✓fully proved

Let \(T > 0\) and, for \(n \in \mathbb{Z}\), let \(e_n(t) = e^{2\pi i n t / T}\) be the \(n\)-th Fourier character on the circle \(\mathbb{R}/T\mathbb{Z}\). With respect to the Haar probability measure on the circle, \(\int e_n = 1\) if \(n = 0\) and \(\int e_n = 0\) otherwise. This is the orthogonality of the Fourier basis.

theorem integral_fourier (n : ℤ) :
    ∫ t : AddCircle T, fourier n t ∂haarAddCircle =
    if n = 0 then 1 else 0

Used by 1

Used byThe Dirichlet kernel has integral one

TheoremThe Dirichlet kernel has integral one#✓fully proved

Let \(T > 0\), let \(e_n(t) = e^{2\pi i n t / T}\) be the \(n\)-th Fourier character on the circle \(\mathbb{R}/T\mathbb{Z}\), and for \(k \in \mathbb{N}\) let \(D_k = \sum_{n=-k}^{k} e_n\) be the \(k\)-th Dirichlet kernel. With respect to the Haar probability measure on the circle, \(\int D_k = 1\); only the term \(n = 0\) contributes, by orthogonality.

theorem integral_dirichlet_sum (k : ℕ) :
    ∫ t : AddCircle T, ∑ n ∈ Finset.Icc (-(k : ℤ)) (k : ℤ),
      fourier n t ∂haarAddCircle = 1

Uses 2 · Used by 1

Proof usesIntegrability of Fourier characters · Integral of a Fourier character

Used byThe Fejér kernel has integral one

TheoremSymmetry of the Fejér kernel#✓fully proved

Let \(T > 0\). For every natural number \(N\) and every \(x \in \mathbb{R}/T\mathbb{Z}\), the \(N\)-th Fejér kernel satisfies \(K_N(-x) = K_N(x)\).

theorem fejerKernel_symmetric (N : ℕ) (x : AddCircle T) :
    fejerKernel N (-x) = fejerKernel N x

Uses 1 · Used by 1

Statement usesThe Fejér kernel

Used byProperties of the Fejér kernel

TheoremThe Fejér kernel has integral one#✓fully proved

Let \(T > 0\) and \(N \in \mathbb{N}\). The \(N\)-th Fejér kernel \(K_N\) on the circle \(\mathbb{R}/T\mathbb{Z}\) satisfies \(\int K_N = 1\) with respect to the Haar probability measure on the circle. This is one of the defining properties of an approximation to the identity.

theorem integral_fejerKernel (N : ℕ) :
    ∫ t : AddCircle T, fejerKernel N t ∂haarAddCircle = 1

Uses 3 · Used by 3

Statement usesThe Fejér kernel

Proof usesIntegrability of Fourier characters · The Dirichlet kernel has integral one

Used byQuantitative Fejér theorem · Properties of the Fejér kernel · The Fejér kernel has \(L^1\) norm one

TheoremPointwise bound for the Fejér kernel#✓fully proved

Let \(T > 0\) and \(N \in \mathbb{N}\). For every point \(x\) of the circle \(\mathbb{R}/T\mathbb{Z}\), the \(N\)-th Fejér kernel satisfies \(|K_N(x)| \le N + 1\).

This follows from the triangle inequality applied to the iterated Dirichlet sum defining \(K_N\), together with \(\sum_{k=0}^{N} (2k+1) = (N+1)^2\).

theorem norm_fejerKernel_le (N : ℕ) (x : AddCircle T) :
    ‖fejerKernel N x‖ ≤ (N : ℝ) + 1

Uses 1 · Used by 1

Statement usesThe Fejér kernel

Used byIntegrability of the Fejér kernel

TheoremContinuity of the Fejér kernel#✓fully proved

Let \(T > 0\). For every natural number \(N\), the \(N\)-th Fejér kernel \(K_N\) is a continuous function from the circle \(\mathbb{R}/T\mathbb{Z}\) to \(\mathbb{C}\).

theorem fejerKernel_continuous (N : ℕ) : Continuous (fejerKernel (T := T) N)

Uses 1 · Used by 2

Statement usesThe Fejér kernel

Used byQuantitative Fejér theorem · Integrability of the Fejér kernel

TheoremIntegrability of the Fejér kernel#✓fully proved

Let \(T > 0\). For every natural number \(N\), the \(N\)-th Fejér kernel \(K_N\) is integrable on the circle \(\mathbb{R}/T\mathbb{Z}\) with respect to the normalized Haar measure, the Haar measure of total mass \(1\).

theorem fejerKernel_integrable (N : ℕ) :
    Integrable (fejerKernel (T := T) N) haarAddCircle

Uses 3 · Used by 2

Statement usesThe Fejér kernel

Proof usesContinuity of the Fejér kernel · Pointwise bound for the Fejér kernel

Used byQuantitative Fejér theorem · The Fejér kernel has \(L^1\) norm one

TheoremProducts of Fourier characters#✓fully proved

Let \(T\) be a real number and, for \(n \in \mathbb{Z}\), let \(e_n\) be the \(n\)-th Fourier character on \(\mathbb{R}/T\mathbb{Z}\), given by \(e_n(x) = e^{2\pi i n x / T}\) (the constant \(1\) when \(T = 0\)). For every integer \(n\) and all \(x, t \in \mathbb{R}/T\mathbb{Z}\), we have \(e_{-n}(t)\, e_n(x) = e_n(x - t)\).

theorem fourier_neg_mul_fourier_eq (n : ℤ) (x t : AddCircle T) :
    (fourier (-n) t : ℂ) * (fourier n x : ℂ) = (fourier n (x - t) : ℂ)

Used by 1

Used byFourier characters at a difference

LemmaReindexing a sum of Fourier characters, negative range#✓fully proved

Let \(T > 0\), let \(e_n(t) = e^{2\pi i n t / T}\) be the \(n\)-th Fourier character on the circle \(\mathbb{R}/T\mathbb{Z}\), and let \(N \in \mathbb{N}\). For every point \(x\) of the circle, \(\sum_{k=0}^{N} e_{k-(N+1)}(x) = \sum_{n=-(N+1)}^{-1} e_n(x)\).

It is used in the proof that the iterated Dirichlet sum defining the Fejér kernel equals \(\left|\sum_{k=0}^{N} e_k(x)\right|^2\).

lemma sum_range_fourier_shift_neg (N : ℕ) (x : AddCircle T) :
    ∑ k ∈ range (N + 1), (fourier ((↑k : ℤ) + -↑(N + 1)) x : ℂ) =
    ∑ n ∈ Finset.Icc (-(↑(N + 1) : ℤ)) (-1 : ℤ), (fourier n x : ℂ)

Used by 1

Used byThe sum of Dirichlet kernels is a squared modulus

LemmaReindexing a sum of Fourier characters, positive range#✓fully proved

Let \(T > 0\), let \(e_n(t) = e^{2\pi i n t / T}\) be the \(n\)-th Fourier character on the circle \(\mathbb{R}/T\mathbb{Z}\), and let \(N \in \mathbb{N}\). For every point \(x\) of the circle, \(\sum_{k=0}^{N} e_{(N+1)-k}(x) = \sum_{n=1}^{N+1} e_n(x)\).

lemma sum_range_fourier_shift_pos (N : ℕ) (x : AddCircle T) :
    ∑ k ∈ range (N + 1), (fourier ((↑(N + 1) : ℤ) + -↑k) x : ℂ) =
    ∑ n ∈ Finset.Icc (1 : ℤ) (↑(N + 1)), (fourier n x : ℂ)

Used by 1

Used byThe sum of Dirichlet kernels is a squared modulus

TheoremThe sum of Dirichlet kernels is a squared modulus#✓fully proved

Let \(T > 0\) and, for \(n \in \mathbb{Z}\), let \(e_n(x) = e^{2\pi i n x / T}\) be the \(n\)-th Fourier character on the circle \(\mathbb{R}/T\mathbb{Z}\). For every natural number \(N\) and every \(x \in \mathbb{R}/T\mathbb{Z}\), put \(G = \sum_{k=0}^{N} e_k(x)\). Then the iterated sum of Dirichlet kernels satisfies \(\sum_{k=0}^{N} \sum_{n=-k}^{k} e_n(x) = G\,\overline{G} = |G|^2\).

theorem fejer_dirichlet_sum_eq_sq (N : ℕ) (x : AddCircle T) :
    (∑ k ∈ range (N + 1), ∑ n ∈ Finset.Icc (-(k : ℤ)) (↑k), (fourier n x : ℂ)) =
    (∑ k ∈ range (N + 1), (fourier (↑k : ℤ) x : ℂ)) *
    starRingEnd ℂ (∑ k ∈ range (N + 1), (fourier (↑k : ℤ) x : ℂ))

Uses 2 · Used by 3

Proof usesReindexing a sum of Fourier characters, negative range · Reindexing a sum of Fourier characters, positive range

Used byThe Fejér kernel as a squared modulus · Nonnegativity of the Fejér kernel · Properties of the Fejér kernel

TheoremNonnegativity of the Fejér kernel#✓fully proved

Let \(T > 0\). For every natural number \(N\) and every \(x \in \mathbb{R}/T\mathbb{Z}\), the real part of the \(N\)-th Fejér kernel at \(x\) is nonnegative: \(\operatorname{Re} K_N(x) \ge 0\).

theorem fejerKernel_nonneg (N : ℕ) (x : AddCircle T) :
    0 ≤ (fejerKernel N x).re

Uses 2 · Used by 1

Statement usesThe Fejér kernel

Proof usesThe sum of Dirichlet kernels is a squared modulus

Used byProperties of the Fejér kernel

TheoremThe Fejér kernel as a squared modulus#✓fully proved

Let \(T > 0\) and, for \(k \in \mathbb{Z}\), let \(e_k(x) = e^{2\pi i k x / T}\) be the \(k\)-th Fourier character on the circle \(\mathbb{R}/T\mathbb{Z}\). For every natural number \(N\) and every \(x \in \mathbb{R}/T\mathbb{Z}\), the \(N\)-th Fejér kernel satisfies \(K_N(x) = \frac{1}{N+1} \left|\sum_{k=0}^{N} e_k(x)\right|^2\).

In particular \(K_N(x)\) is a nonnegative real number, so \(|K_N(x)| = \operatorname{Re} K_N(x)\).

theorem fejerKernel_eq_ofReal (N : ℕ) (x : AddCircle T) :
    fejerKernel N x = ↑(((N : ℝ) + 1)⁻¹ *
      normSq (∑ k ∈ range (N + 1), (fourier (↑k : ℤ) x : ℂ)))

Uses 2 · Used by 1

Statement usesThe Fejér kernel

Proof usesThe sum of Dirichlet kernels is a squared modulus

Used byThe Fejér kernel has \(L^1\) norm one

TheoremProperties of the Fejér kernel#✓fully proved

Let \(T > 0\), let \(N\) be a natural number, let \(K_N\) be the \(N\)-th Fejér kernel on the circle \(\mathbb{R}/T\mathbb{Z}\), let \(\mu\) be the normalized Haar measure on \(\mathbb{R}/T\mathbb{Z}\) (of total mass \(1\)), and let \(e_1(x) = e^{2\pi i x / T}\). Then \(\operatorname{Re} K_N(x) \ge 0\) for every \(x \in \mathbb{R}/T\mathbb{Z}\); \(K_N(-x) = K_N(x)\) for every \(x \in \mathbb{R}/T\mathbb{Z}\); the function on \(\mathbb{R}\) sending \(t\) to \(K_N\) evaluated at the class of \(t\) in \(\mathbb{R}/T\mathbb{Z}\) is \(T\)-periodic; \(\int K_N \, d\mu = 1\); and for every \(\delta > 0\) and every \(x \in \mathbb{R}/T\mathbb{Z}\) with \(\delta \le |1 - e_1(x)|\) we have \(|K_N(x)| \le \frac{4}{(N+1)\delta^2}\).

theorem fejer_kernel_properties (N : ℕ) :
    (∀ x : AddCircle T, 0 ≤ (fejerKernel N x).re) ∧
    (∀ x : AddCircle T, fejerKernel N (-x) = fejerKernel N x) ∧
    (Function.Periodic (fun t : ℝ => fejerKernel (T := T) N (↑t)) T) ∧
    (∫ t : AddCircle T, fejerKernel N t ∂haarAddCircle = 1) ∧
    (∀ δ : ℝ, 0 < δ → ∀ x : AddCircle T,
      δ ≤ ‖(1 : ℂ) - fourier (1 : ℤ) x‖ →
      ‖fejerKernel N x‖ ≤ 4 / (((N : ℝ) + 1) * δ ^ 2))

Uses 5 · Used by 1

Statement usesThe Fejér kernel

Proof usesNonnegativity of the Fejér kernel · Symmetry of the Fejér kernel · The sum of Dirichlet kernels is a squared modulus · The Fejér kernel has integral one

Used byQuantitative Fejér theorem

DefinitionPartial Fourier sums#✓fully proved

Let \(T > 0\) and \(f : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\). For \(N \in \mathbb{N}\), the \(N\)-th partial Fourier sum of \(f\) is the function

\[S_N f(x) = \sum_{n=-N}^{N} \hat f(n)\, e_n(x),\]

where \(e_n(x) = e^{2\pi i n x / T}\) is the \(n\)-th Fourier character and \(\hat f(n) = \int_{\mathbb{R}/T\mathbb{Z}} e_{-n}(t)\, f(t)\, dt\) is the \(n\)-th Fourier coefficient, the integral taken against the Haar probability measure on the circle.

noncomputable def partialFourierSum (f : AddCircle T → ℂ) (N : ℕ) :
    AddCircle T → ℂ :=
  fun x => ∑ n ∈ Finset.Icc (-(N : ℤ)) (N : ℤ), fourierCoeff f n • fourier n x

Used by 2

Used byCesàro–Fourier means · Cesàro–Fourier means are convolutions with the Fejér kernel

DefinitionCesàro–Fourier means#✓fully proved

Let \(T > 0\) and \(f : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\). For \(N \in \mathbb{N}\), the \(N\)-th Cesàro–Fourier mean of \(f\) is the average of its first \(N + 1\) partial Fourier sums,

\[\sigma_N f(x) = \frac{1}{N+1} \sum_{k=0}^{N} S_k f(x),\]

where \(S_k f\) is the \(k\)-th partial Fourier sum of \(f\).

noncomputable def cesaroFourierMean (f : AddCircle T → ℂ) (N : ℕ) :
    AddCircle T → ℂ :=
  fun x => ((N : ℂ) + 1)⁻¹ • ∑ k ∈ range (N + 1), partialFourierSum f k x

Uses 1 · Used by 3

Statement usesPartial Fourier sums

Used byCesàro–Fourier means are convolutions with the Fejér kernel · Quantitative Fejér theorem · Fejér's theorem: uniform convergence of Cesàro–Fourier means

LemmaFourier characters at a difference#✓fully proved

Let \(T > 0\) and for \(n \in \mathbb{Z}\) let \(e_n(x) = e^{2\pi i n x / T}\) be the \(n\)-th Fourier character on \(\mathbb{R}/T\mathbb{Z}\). Then for every \(n \in \mathbb{Z}\) and all \(x, t \in \mathbb{R}/T\mathbb{Z}\), \(e_n(x - t) = e_{-n}(t)\, e_n(x)\).

lemma fourier_sub_eq (n : ℤ) (x t : AddCircle T) :
    (fourier n (x - t) : ℂ) = (fourier (-n) t : ℂ) * (fourier n x : ℂ)

Uses 1 · Used by 1

Proof usesProducts of Fourier characters

Used byConvolution of a function with a Fourier character

LemmaIntegrability of a function twisted by a Fourier character#✓fully proved

Let \(T > 0\) and let \(f : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\) be integrable with respect to the Haar probability measure on the circle. Then for every \(n \in \mathbb{Z}\) and every \(x \in \mathbb{R}/T\mathbb{Z}\), the function \(t \mapsto e^{2\pi i n t / T} f(x - t)\) is integrable with respect to the same measure.

This is used to interchange sums and integrals in the convolution computation.

lemma fourier_smul_integrable (f : AddCircle T → ℂ) (hf : Integrable f haarAddCircle)
    (n : ℤ) (x : AddCircle T) :
    Integrable (fun t => (fourier n t : ℂ) • f (x - t)) haarAddCircle

Used by 1

Used byCesàro–Fourier means are convolutions with the Fejér kernel

TheoremConvolution of a function with a Fourier character#✓fully proved

Let \(T > 0\), let \(f : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\) be integrable with respect to the Haar probability measure \(dt\) on the circle, for \(n \in \mathbb{Z}\) let \(e_n(x) = e^{2\pi i n x / T}\) be the \(n\)-th Fourier character, and let \(\hat f(n) = \int_{\mathbb{R}/T\mathbb{Z}} e_{-n}(t)\, f(t)\, dt\) be the \(n\)-th Fourier coefficient of \(f\). Then for every \(n \in \mathbb{Z}\) and every \(x \in \mathbb{R}/T\mathbb{Z}\),

\[\int_{\mathbb{R}/T\mathbb{Z}} e_n(t)\, f(x - t)\, dt = \hat f(n)\, e_n(x).\]

Thus the \(n\)-th term of the partial Fourier sum of \(f\) at \(x\) is the convolution of \(f\) with the Fourier character \(e_n\).

theorem fourier_integral_convolution (f : AddCircle T → ℂ)
    (_hf : Integrable f haarAddCircle) (n : ℤ) (x : AddCircle T) :
    ∫ t : AddCircle T, (fourier n t : ℂ) • f (x - t) ∂haarAddCircle =
    fourierCoeff f n • (fourier n x : ℂ)

Uses 1 · Used by 1

Proof usesFourier characters at a difference

Used byCesàro–Fourier means are convolutions with the Fejér kernel

TheoremCesàro–Fourier means are convolutions with the Fejér kernel#✓fully proved

Let \(T > 0\) and let \(f : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\) be integrable with respect to the Haar probability measure \(dt\) on the circle. Then for every \(N \in \mathbb{N}\) and every \(x \in \mathbb{R}/T\mathbb{Z}\), the \(N\)-th Cesàro–Fourier mean of \(f\) satisfies

\[\sigma_N f(x) = \int_{\mathbb{R}/T\mathbb{Z}} K_N(t)\, f(x - t)\, dt,\]

where \(K_N\) is the \(N\)-th Fejér kernel.

This is the bridge from the definition of \(\sigma_N f\) to the kernel-theoretic analysis underlying Fejér's theorem.

theorem cesaroMean_eq_fejer_convolution (f : AddCircle T → ℂ)
    (hf : Integrable f haarAddCircle) (N : ℕ) (x : AddCircle T) :
    cesaroFourierMean f N x =
    ∫ t : AddCircle T, fejerKernel N t • f (x - t) ∂haarAddCircle

Uses 5 · Used by 1

Statement usesCesàro–Fourier means · The Fejér kernel

Proof usesConvolution of a function with a Fourier character · Integrability of a function twisted by a Fourier character · Partial Fourier sums

Used byQuantitative Fejér theorem

TheoremThe Fejér kernel has \(L^1\) norm one#✓fully proved

Let \(T > 0\). For every \(N \in \mathbb{N}\), the \(N\)-th Fejér kernel \(K_N\) on \(\mathbb{R}/T\mathbb{Z}\) satisfies

\[\int_{\mathbb{R}/T\mathbb{Z}} |K_N(t)|\, dt = 1,\]

where \(dt\) is the Haar probability measure on the circle.

Since \(K_N \ge 0\), this is the normalization \(\int K_N = 1\); it is used to control convolutions with \(K_N\) in the proof of Fejér's theorem.

theorem integral_norm_fejerKernel (N : ℕ) :
    ∫ t : AddCircle T, ‖fejerKernel N t‖ ∂haarAddCircle = 1

Uses 4 · Used by 1

Statement usesThe Fejér kernel

Proof usesThe Fejér kernel as a squared modulus · Integrability of the Fejér kernel · The Fejér kernel has integral one

Used byQuantitative Fejér theorem

TheoremQuantitative Fejér theorem#✓fully proved

Let \(T > 0\), let \(f\) be a continuous complex-valued function on the circle \(\mathbb{R}/T\mathbb{Z}\), and write \(\sigma_N f\) for its \(N\)-th Cesàro–Fourier mean. Let \(\varepsilon > 0\) and \(\delta > 0\) be such that \(|f(a) - f(b)| < \varepsilon / 2\) for all points \(a, b\) of the circle at distance less than \(\delta\). Then there is \(N_0 \in \mathbb{N}\) such that \(|f(x) - \sigma_N f(x)| < \varepsilon\) for every \(N \ge N_0\) and every point \(x\) of the circle.

The proof writes \(f(x) - \sigma_N f(x) = \int K_N(t)\,(f(x) - f(x - t))\,dt\), where \(K_N\) is the \(N\)-th Fejér kernel and the integral is against the Haar probability measure, and splits it into the points \(t\) at distance less than \(\delta\) from \(0\), where \(f(x) - f(x - t)\) is small, and the remaining points, where the Fejér kernel is \(O(1/((N+1)\delta^2))\).

theorem cesaroMean_uniform_bound (f : C(AddCircle T, ℂ))
    (ε : ℝ) (hε : 0 < ε) (δ : ℝ) (hδ_pos : 0 < δ)
    (hδ : ∀ ⦃a b : AddCircle T⦄, dist a b < δ → dist (f a) (f b) < ε / 2) :
    ∃ N₀ : ℕ, ∀ N ≥ N₀, ∀ x : AddCircle T,
      dist (f x) (cesaroFourierMean (⇑f) N x) < ε

Uses 8 · Used by 1

Statement usesCesàro–Fourier means

Proof usesCesàro–Fourier means are convolutions with the Fejér kernel · The Fejér kernel · Continuity of the Fejér kernel · Integrability of the Fejér kernel · Properties of the Fejér kernel · The Fejér kernel has integral one · The Fejér kernel has \(L^1\) norm one

Used byFejér's theorem: uniform convergence of Cesàro–Fourier means

TheoremFejér's theorem: uniform convergence of Cesàro–Fourier means#✓fully proved

Let \(T > 0\) and let \(f\) be a continuous complex-valued function on the circle \(\mathbb{R}/T\mathbb{Z}\) (equivalently, a continuous \(T\)-periodic function on \(\mathbb{R}\)). Then the Cesàro–Fourier means \(\sigma_N f\) converge to \(f\) uniformly on the circle as \(N \to \infty\).

theorem fejer_uniform_convergence (f : C(AddCircle T, ℂ)) :
    TendstoUniformly (fun N => cesaroFourierMean (⇑f) N) (⇑f) atTop

Uses 2

Statement usesCesàro–Fourier means

Proof usesQuantitative Fejér theorem

25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.