Documentation

Atlas.IntroductionToFunctionalAnalysis.code.FourierSeries

noncomputable def FourierSeries.partialFourierSum {T : } [hT : Fact (0 < T)] (f : AddCircle T) (N : ) :

The N-th partial Fourier sum of a function f : AddCircle T → ℂ, defined as S_N f(x) = ∑_{n = -N}^{N} ĉ_n(f) · e^{2πi n x / T}, where ĉ_n(f) = fourierCoeff f n.

Instances For
    noncomputable def FourierSeries.cesaroFourierMean {T : } [hT : Fact (0 < T)] (f : AddCircle T) (N : ) :

    The N-th Cesàro–Fourier mean of f, given by σ_N f(x) = (N+1)⁻¹ · ∑_{k=0}^{N} S_k f(x), where S_k f is the k-th partial Fourier sum.

    Instances For
      noncomputable def FourierSeries.fejerKernel {T : } (N : ) :

      The Fejér kernel K_N, defined here as the Cesàro mean of the Dirichlet kernels: K_N(x) = (N+1)⁻¹ · ∑_{k=0}^{N} ∑_{n=-k}^{k} e^{2πi n x / T}. Equivalently (after algebra), K_N(x) = (N+1)⁻¹ · (sin((N+1)x/2) / sin(x/2))² away from the origin.

      Instances For

        Each Fourier mode t ↦ e^{2πi n t / T} is integrable on the circle (in fact bounded by 1); used repeatedly when integrating Fourier sums termwise.

        theorem FourierSeries.integral_fourier {T : } [hT : Fact (0 < T)] (n : ) :

        Orthogonality of the Fourier basis with respect to the Haar measure: the integral of e^{2πi n t / T} over the circle equals 1 if n = 0 and 0 otherwise.

        theorem FourierSeries.integral_dirichlet_sum {T : } [hT : Fact (0 < T)] (k : ) :
        (t : AddCircle T), nFinset.Icc (-k) k, (fourier n) t AddCircle.haarAddCircle = 1

        The integral of the k-th Dirichlet kernel ∑_{n=-k}^{k} e^{2πi n t / T} over the circle equals 1; only the n = 0 term contributes by orthogonality.

        theorem FourierSeries.fejerKernel_symmetric {T : } [hT : Fact (0 < T)] (N : ) (x : AddCircle T) :

        Symmetry of the Fejér kernel: K_N(-x) = K_N(x) for every x ∈ AddCircle T.

        The Fejér kernel integrates to 1 on the circle: ∫_{AddCircle T} K_N(t) dt = 1. This is one of the defining properties of an approximation to the identity.

        theorem FourierSeries.norm_fejerKernel_le {T : } [hT : Fact (0 < T)] (N : ) (x : AddCircle T) :

        Pointwise bound ‖K_N(x)‖ ≤ N + 1, obtained from the triangle inequality applied to the iterated Dirichlet sum together with ∑_{k=0}^{N}(2k+1) = (N+1)².

        The Fejér kernel K_N is continuous on AddCircle T, being a finite linear combination of continuous Fourier modes.

        The Fejér kernel K_N is integrable on the circle; this follows from continuity together with the pointwise bound ‖K_N‖ ≤ N + 1.

        theorem FourierSeries.fourier_neg_mul_fourier_eq {T : } (n : ) (x t : AddCircle T) :
        (fourier (-n)) t * (fourier n) x = (fourier n) (x - t)

        Convolution identity for Fourier modes: e^{-2πi n t / T} · e^{2πi n x / T} = e^{2πi n (x - t) / T}. The basic shift identity behind expressing partial Fourier sums as convolutions with the Dirichlet kernel.

        theorem FourierSeries.sum_range_fourier_shift_neg {T : } [hT : Fact (0 < T)] (N : ) (x : AddCircle T) :
        kFinset.range (N + 1), (fourier (k + -↑(N + 1))) x = nFinset.Icc (-↑(N + 1)) (-1), (fourier n) x

        Re-indexing lemma: the sum ∑_{k=0}^{N} e^{2πi (k - (N+1)) x / T} equals the sum over the negative range n ∈ [-(N+1), -1]. Used to expand (∑ z^k) · z̄^{N+1} in the proof of the Fejér kernel identity.

        theorem FourierSeries.sum_range_fourier_shift_pos {T : } [hT : Fact (0 < T)] (N : ) (x : AddCircle T) :
        kFinset.range (N + 1), (fourier (↑(N + 1) + -k)) x = nFinset.Icc 1 ↑(N + 1), (fourier n) x

        Companion to sum_range_fourier_shift_neg: the sum ∑_{k=0}^{N} e^{2πi ((N+1) - k) x / T} equals the sum over the positive range n ∈ [1, N+1].

        theorem FourierSeries.fejer_dirichlet_sum_eq_sq {T : } [hT : Fact (0 < T)] (N : ) (x : AddCircle T) :
        kFinset.range (N + 1), nFinset.Icc (-k) k, (fourier n) x = (∑ kFinset.range (N + 1), (fourier k) x) * (starRingEnd ) (∑ kFinset.range (N + 1), (fourier k) x)

        Key algebraic identity: the iterated Dirichlet sum defining K_N equals |∑_{k=0}^{N} e^{2πi k x / T}|², i.e. a sum-of-Dirichlet kernels is the squared modulus of a geometric sum. This is what makes the Fejér kernel nonnegative.

        theorem FourierSeries.fejerKernel_nonneg {T : } [hT : Fact (0 < T)] (N : ) (x : AddCircle T) :

        Positivity of the Fejér kernel: 0 ≤ Re K_N(x) for every x. Direct consequence of the expression K_N(x) = (N+1)⁻¹ · |∑_{k=0}^N e^{2πi k x / T}|².

        theorem FourierSeries.fejer_kernel_properties {T : } [hT : Fact (0 < T)] (N : ) :
        (∀ (x : AddCircle T), 0 (fejerKernel N x).re) (∀ (x : AddCircle T), fejerKernel N (-x) = fejerKernel N x) Function.Periodic (fun (t : ) => fejerKernel N t) T (t : AddCircle T), fejerKernel N t AddCircle.haarAddCircle = 1 ∀ (δ : ), 0 < δ∀ (x : AddCircle T), δ 1 - (fourier 1) xfejerKernel N x 4 / ((N + 1) * δ ^ 2)

        Bundled properties of the Fejér kernel K_N on AddCircle T: (1) K_N(x) ≥ 0 for all x, (2) K_N is symmetric: K_N(-x) = K_N(x), (3) K_N is T-periodic on , (4) ∫ K_N = 1, and (5) the decay estimate: for any δ > 0 and any x with δ ≤ ‖1 - e^{2πi x / T}‖, we have ‖K_N(x)‖ ≤ 4 / ((N+1) δ²).

        theorem FourierSeries.fourier_sub_eq {T : } [hT : Fact (0 < T)] (n : ) (x t : AddCircle T) :
        (fourier n) (x - t) = (fourier (-n)) t * (fourier n) x

        Reversed form of fourier_neg_mul_fourier_eq: e^{2πi n (x - t) / T} = e^{-2πi n t / T} · e^{2πi n x / T}. Convenient orientation for the convolution computation.

        If f is integrable on AddCircle T, then t ↦ e^{2πi n t / T} · f(x - t) is also integrable; a routine integrability lemma needed to interchange sums and integrals in the convolution computation.

        Convolution-with-a-mode identity: for integrable f, ∫ e^{2πi n t / T} · f(x - t) dt = ĉ_n(f) · e^{2πi n x / T}. This says that the n-th term of the partial Fourier sum at x is the convolution of f with the mode e^{2πi n · / T}.

        The Cesàro–Fourier mean as a convolution against the Fejér kernel: σ_N f(x) = ∫_{AddCircle T} K_N(t) · f(x - t) dt, valid for any integrable f. This is the bridge from the abstract definition of σ_N f to the kernel-theoretic analysis underlying Fejér's theorem.

        theorem fejerKernel_eq_ofReal {T : } [hT : Fact (0 < T)] (N : ) (x : AddCircle T) :
        FourierSeries.fejerKernel N x = ↑((N + 1)⁻¹ * Complex.normSq (∑ kFinset.range (N + 1), (fourier k) x))

        The Fejér kernel is in fact a nonnegative real number (coerced into ): K_N(x) = (N+1)⁻¹ · |∑_{k=0}^{N} e^{2πi k x / T}|², written with normSq. This makes ‖K_N(x)‖ = Re K_N(x).

        Since K_N ≥ 0, its norm coincides with its integral: ∫ ‖K_N(t)‖ dt = 1. Used to control the convolution ‖K_N * (f - f(x - ·))‖ in the proof of Fejér's theorem.

        theorem cesaroMean_uniform_bound {T : } [hT : Fact (0 < T)] (f : C(AddCircle T, )) (ε : ) ( : 0 < ε) (δ : ) (hδ_pos : 0 < δ) ( : ∀ ⦃a b : AddCircle T⦄, dist a b < δdist (f a) (f b) < ε / 2) :
        ∃ (N₀ : ), NN₀, ∀ (x : AddCircle T), dist (f x) (FourierSeries.cesaroFourierMean (⇑f) N x) < ε

        Quantitative form of Fejér's theorem: given ε > 0 and a modulus of continuity δ > 0 for f ∈ C(AddCircle T, ℂ) at scale ε/2, there exists N₀ such that ∀ N ≥ N₀, ∀ x, dist (f x) (σ_N f x) < ε. The proof splits the convolution integral into the region ‖t‖ < δ (where f(x) − f(x − t) is small) and its complement (where the Fejér kernel decays as O(1/((N+1)δ²))).

        theorem fejer_uniform_convergence {T : } [hT : Fact (0 < T)] (f : C(AddCircle T, )) :

        Fejér's theorem on AddCircle T: for every continuous function f : AddCircle T → ℂ (equivalently, every continuous T-periodic function on ), the Cesàro–Fourier means σ_N f converge uniformly to f as N → ∞.