theorem helperForTheorem_5_4_1_dense_span_witness (f : C(AddCircle 1, ℂ)) (ε : ℝ) (hε : 0 < ε) : ∃ P ∈ Submodule.span ℂ (Set.range fourier), ‖f - P‖ < ε

Helper for Theorem 5.4.1: extract a Fourier-span element that approximates a target continuous function within a prescribed sup-norm error.

theorem helperForTheorem_5_4_1_span_element_has_finsupp_expansion {P : C(AddCircle 1, ℂ)} (hP : P ∈ Submodule.span ℂ (Set.range fourier)) : ∃ (c : ℤ →₀ ℂ), P = c.sum fun (n : ℤ) (a : ℂ) => a • fourierCharacter n

Helper for Theorem 5.4.1: every element of the Fourier span has a finite Finsupp expansion in the characters fourierCharacter n.

theorem helperForTheorem_5_4_1_support_in_symmetric_Icc (c : ℤ →₀ ℂ) : have N := c.support.sup Int.natAbs; ∀ n ∈ c.support, n ∈ Finset.Icc (-↑N) ↑N

Helper for Theorem 5.4.1: the support of a finitely supported coefficient family is contained in a symmetric interval [-N, N], with N = c.support.sup Int.natAbs.

theorem helperForTheorem_5_4_1_isTrig_of_finsupp_expansion (c : ℤ →₀ ℂ) : IsTrigonometricPolynomial (c.sum fun (n : ℤ) (a : ℂ) => a • fourierCharacter n)

Helper for Theorem 5.4.1: every finite Fourier-character expansion is a trigonometric polynomial in the sense of Definition 5.3.2.

theorem exists_trigonometricPolynomial_uniform_approximation (f : C(AddCircle 1, ℂ)) (ε : ℝ) (hε : 0 < ε) : ∃ (P : C(AddCircle 1, ℂ)), IsTrigonometricPolynomial P ∧ ‖f - P‖ ≤ ε

Theorem 5.4.1 (Weierstrass approximation theorem for trigonometric polynomials): for every continuous function f : C(ℝ/ℤ; ℂ) and every ε > 0, there exists a trigonometric polynomial P such that ‖f - P‖ ≤ ε.

theorem periodicConvolution_continuous (f g : C(AddCircle 1, ℂ)) : Continuous fun (x : AddCircle 1) => ∫ (y : ℝ) in Set.Icc 0 1, f ↑y * g (x - ↑y)

Continuity of the function underlying periodic convolution.

noncomputable def periodicConvolution (f g : C(AddCircle 1, ℂ)) : C(AddCircle 1, ℂ)

Definition 5.4.2: for continuous f, g : C(ℝ/ℤ; ℂ), the periodic convolution is the continuous function on ℝ/ℤ given by (f * g)(x) = ∫ y ∈ [0,1], f(y) g(x - y) dy with y viewed in ℝ/ℤ.

Equations

• periodicConvolution f g = { toFun := fun (x : AddCircle 1) => ∫ (y : ℝ) in Set.Icc 0 1, f ↑y * g (x - ↑y), continuous_toFun := ⋯ }

theorem periodicConvolution_continuous_closure (f g : C(AddCircle 1, ℂ)) : Continuous ⇑(periodicConvolution f g)

Lemma 5.4.4a (Basic properties of periodic convolution (a), Closure): if f, g ∈ C(ℝ/ℤ; ℂ), then f * g ∈ C(ℝ/ℤ; ℂ). In this file, f * g is represented by periodicConvolution f g.

theorem helperForLemma_5_4_4b_eval_eq_addcircle_convolution (f g : C(AddCircle 1, ℂ)) (x : AddCircle 1) : ∫ (y : ℝ) in Set.Icc 0 1, f ↑y * g (x - ↑y) = MeasureTheory.convolution (fun (t : AddCircle 1) => f t) (fun (t : AddCircle 1) => g t) (ContinuousLinearMap.mul ℂ ℂ) MeasureTheory.volume x

Helper for Lemma 5.4.4b: rewrite the periodic-convolution integral on Set.Icc as an evaluation of convolution on AddCircle (1 : ℝ).

theorem helperForLemma_5_4_4b_mul_convolution_eq_flip_convolution (F G : AddCircle 1 → ℂ) : MeasureTheory.convolution G F (ContinuousLinearMap.mul ℂ ℂ) MeasureTheory.volume = MeasureTheory.convolution G F (ContinuousLinearMap.mul ℂ ℂ).flip MeasureTheory.volume

Helper for Lemma 5.4.4b: for complex-valued convolution, replacing mul by mul.flip does not change the result.

theorem helperForLemma_5_4_4b_addcircle_convolution_comm (F G : AddCircle 1 → ℂ) : MeasureTheory.convolution F G (ContinuousLinearMap.mul ℂ ℂ) MeasureTheory.volume = MeasureTheory.convolution G F (ContinuousLinearMap.mul ℂ ℂ) MeasureTheory.volume

Helper for Lemma 5.4.4b: convolution on AddCircle (1 : ℝ) with complex multiplication is commutative.

theorem periodicConvolution_comm (f g : C(AddCircle 1, ℂ)) : periodicConvolution f g = periodicConvolution g f

Lemma 5.4.4b (Basic properties of periodic convolution (b), Commutativity): for f, g : C(ℝ/ℤ; ℂ), one has f * g = g * f, represented here as periodicConvolution f g = periodicConvolution g f.

theorem periodicConvolution_bilinearity (f g h : C(AddCircle 1, ℂ)) (c : ℂ) : periodicConvolution f (g + h) = periodicConvolution f g + periodicConvolution f h ∧ periodicConvolution (f + g) h = periodicConvolution f h + periodicConvolution g h ∧ c • periodicConvolution f g = periodicConvolution (c • f) g ∧ periodicConvolution (c • f) g = periodicConvolution f (c • g)

Lemma 5.4.4c (Basic properties of periodic convolution (c), Bilinearity): for f, g, h : C(ℝ/ℤ; ℂ) and c : ℂ, one has f * (g + h) = f * g + f * h, (f + g) * h = f * h + g * h, and c (f * g) = (c f) * g = f * (c g), represented here using periodicConvolution.

theorem helperForLemma_5_4_5_character_sub_factorization (n : ℤ) (x y : AddCircle 1) : (fourierCharacter n) (x - y) = (fourierCharacter n) x * (fourierCharacter (-n)) y

Helper for Lemma 5.4.5: factor a character at a difference into a product of an x-factor and a y-factor.

theorem helperForLemma_5_4_5_intervalIntegral_eq_fourierTransform (f : C(AddCircle 1, ℂ)) (n : ℤ) : ∫ (y : ℝ) in Set.Icc 0 1, f ↑y * (fourierCharacter (-n)) ↑y = fourierTransform f n

Helper for Lemma 5.4.5: identify the interval integral appearing in the character-convolution computation with the Fourier coefficient.

theorem helperForLemma_5_4_5_convolution_right_smul (f g : C(AddCircle 1, ℂ)) (c : ℂ) : periodicConvolution f (c • g) = c • periodicConvolution f g

Helper for Lemma 5.4.5: periodic convolution is scalar-linear in the second argument.

theorem helperForLemma_5_4_5_convolution_with_character (f : C(AddCircle 1, ℂ)) (n : ℤ) : periodicConvolution f (fourierCharacter n) = fourierTransform f n • fourierCharacter n

Helper for Lemma 5.4.5: each Fourier character is an eigenfunction of periodic convolution with eigenvalue equal to the corresponding Fourier coefficient of the left factor.

theorem helperForLemma_5_4_5_convolution_finite_fourier_sum (f : C(AddCircle 1, ℂ)) (N : ℕ) (c : ℤ → ℂ) : periodicConvolution f (∑ k ∈ Finset.Icc (-↑N) ↑N, c k • fourierCharacter k) = ∑ k ∈ Finset.Icc (-↑N) ↑N, (fourierTransform f k * c k) • fourierCharacter k

Helper for Lemma 5.4.5: convolution with a trigonometric polynomial acts termwise on its Fourier expansion.

theorem periodicConvolution_fourierCharacter_and_trigSum (f : C(AddCircle 1, ℂ)) (n : ℤ) (N : ℕ) (c : ℤ → ℂ) : periodicConvolution f (fourierCharacter n) = fourierTransform f n • fourierCharacter n ∧ periodicConvolution f (∑ k ∈ Finset.Icc (-↑N) ↑N, c k • fourierCharacter k) = ∑ k ∈ Finset.Icc (-↑N) ↑N, (fourierTransform f k * c k) • fourierCharacter k ∧ IsTrigonometricPolynomial (periodicConvolution f (∑ k ∈ Finset.Icc (-↑N) ↑N, c k • fourierCharacter k))

Lemma 5.4.5: for f ∈ C(ℝ/ℤ; ℂ) and n ∈ ℤ, one has f * e_n = \hat f(n)e_n. More generally, for a trigonometric polynomial P = ∑_{k=-N}^{N} c_k e_k, periodic convolution acts termwise: f * P = ∑_{k=-N}^{N} \hat f(k)c_k e_k, hence f * P is trigonometric.

def IsPeriodicApproximationToIdentity (ε δ : ℝ) (f : C(AddCircle 1, ℂ)) : Prop

Definition 5.4.5 (Periodic approximation to the identity): for ε > 0 and 0 < δ < 1/2, a continuous periodic function f : C(ℝ/ℤ; ℂ) is a periodic (ε, δ) approximation to the identity iff (a) f(x) is real and nonnegative for all x, and ∫_[0,1] f = 1, and (b) |f(x)| < ε whenever δ ≤ |x| ≤ 1 - δ.

Equations

• One or more equations did not get rendered due to their size.