noncomputable def helperForLemma_5_4_6_fejerPolynomial (N : ℕ) : C(AddCircle 1, ℂ)

Helper for Lemma 5.4.6: Fejér polynomial on AddCircle (1 : ℝ) with frequency cutoff N.

Equations

• helperForLemma_5_4_6_fejerPolynomial N = ∑ k ∈ Finset.Icc (-↑N) ↑N, (↑(N + 1 - k.natAbs) / ↑(N + 1)) • fourierCharacter k

theorem helperForLemma_5_4_6_fejer_isTrig (N : ℕ) : IsTrigonometricPolynomial (helperForLemma_5_4_6_fejerPolynomial N)

Helper for Lemma 5.4.6: the Fejér polynomial is a trigonometric polynomial.

theorem helperForLemma_5_4_6_intervalIntegral_fourierCharacter_eq_ite (k : ℤ) : ∫ (y : ℝ) in Set.Icc 0 1, (fourierCharacter k) ↑y = if k = 0 then 1 else 0

Helper for Lemma 5.4.6: character integral on [0,1] is 1 at frequency 0 and vanishes at nonzero frequencies.

theorem helperForLemma_5_4_6_fejerIntegral_as_weightedCharacterSum (N : ℕ) : ∫ (y : ℝ) in Set.Icc 0 1, (helperForLemma_5_4_6_fejerPolynomial N) ↑y = ∑ k ∈ Finset.Icc (-↑N) ↑N, ↑(N + 1 - k.natAbs) / ↑(N + 1) * ∫ (y : ℝ) in Set.Icc 0 1, (fourierCharacter k) ↑y

Helper for Lemma 5.4.6: rewrite the Fejér mass integral as a weighted finite character-integral sum.

theorem helperForLemma_5_4_6_fejer_mass_one (N : ℕ) : ∫ (y : ℝ) in Set.Icc 0 1, (helperForLemma_5_4_6_fejerPolynomial N) ↑y = 1

Helper for Lemma 5.4.6: the Fejér polynomial has total mass 1 on [0,1].

theorem helperForLemma_5_4_6_chooseIndexFromTailBound {ε C : ℝ} (hε : 0 < ε) (hC : 0 < C) : ∃ (N : ℕ), C / (↑N + 1) < ε

Helper for Lemma 5.4.6: Archimedean index choice turning an O((N+1)⁻¹) bound into a strict < ε estimate.

theorem helperForLemma_5_4_6_intDiff_eq_natShift (i j m : ℕ) : ↑i - ↑j = ↑m ↔ i = j + m

Helper for Lemma 5.4.6: convert an integer-difference equation between natural numbers into a nonnegative shift equation.

theorem helperForLemma_5_4_6_intDiff_eq_negNatShift (i j m : ℕ) : ↑i - ↑j = -↑m ↔ j = i + m

Helper for Lemma 5.4.6: convert an integer-difference equation between natural numbers into a negative shift equation.

theorem helperForLemma_5_4_6_pairCount_nonnegShift (N m : ℕ) : {p ∈ (Finset.range (N + 1)).product (Finset.range (N + 1)) | p.1 = p.2 + m}.card = N + 1 - m

Helper for Lemma 5.4.6: count pairs (i,j) in range (N+1) × range (N+1) with i = j + m.

theorem helperForLemma_5_4_6_pairCount_nonnegShift_swapped (N m : ℕ) : {p ∈ (Finset.range (N + 1)).product (Finset.range (N + 1)) | p.2 = p.1 + m}.card = N + 1 - m

Helper for Lemma 5.4.6: count pairs (i,j) in range (N+1) × range (N+1) with j = i + m.

theorem helperForLemma_5_4_6_pairCount_eq_weight (N : ℕ) (k : ℤ) : {p ∈ (Finset.range (N + 1)).product (Finset.range (N + 1)) | ↑p.1 - ↑p.2 = k}.card = N + 1 - k.natAbs

Helper for Lemma 5.4.6: the number of pairs in range (N+1) × range (N+1) with integer difference k is N+1-|k|.

theorem helperForLemma_5_4_6_diff_mem_Icc (N i j : ℕ) (hi : i ∈ Finset.range (N + 1)) (hj : j ∈ Finset.range (N + 1)) : ↑i - ↑j ∈ Finset.Icc (-↑N) ↑N

Helper for Lemma 5.4.6: integer differences of indices from range (N+1) lie in the symmetric interval [-N, N].

theorem helperForLemma_5_4_6_doubleRangeSum_groupByDifference (N : ℕ) (z : ℂ) : ∑ i ∈ Finset.range (N + 1), ∑ j ∈ Finset.range (N + 1), z ^ i * star (z ^ j) = ∑ k ∈ Finset.Icc (-↑N) ↑N, ∑ p ∈ (Finset.range (N + 1)).product (Finset.range (N + 1)) with ↑p.1 - ↑p.2 = k, z ^ p.1 * star (z ^ p.2)

Helper for Lemma 5.4.6: group the double range sum by fixed difference k = i - j.

theorem helperForLemma_5_4_6_expTerm_onDifferenceFiber (x : ℝ) (i j : ℕ) (k : ℤ) (hDiff : ↑i - ↑j = k) : have z := Complex.exp (Complex.I * (2 * ↑Real.pi * ↑x)); z ^ i * star (z ^ j) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑k * ↑x)

Helper for Lemma 5.4.6: on the fiber where i - j = k, the term z^i * conj(z^j) with z = exp(i 2π x) collapses to the k-mode exponential.

theorem helperForLemma_5_4_6_weightedIccSum_eq_doubleRangeSum (N : ℕ) (x : ℝ) : have z := Complex.exp (Complex.I * (2 * ↑Real.pi * ↑x)); ∑ k ∈ Finset.Icc (-↑N) ↑N, ↑(N + 1 - k.natAbs) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑k * ↑x) = ∑ i ∈ Finset.range (N + 1), ∑ j ∈ Finset.range (N + 1), z ^ i * star (z ^ j)

Helper for Lemma 5.4.6: convert the weighted k-sum on [-N,N] into the double-range geometric sum.

theorem helperForLemma_5_4_6_fejerCoeff_weightedSum_eq_doubleGeomSum (N : ℕ) (x : ℝ) : have z := Complex.exp (Complex.I * (2 * ↑Real.pi * ↑x)); have D := 1 / ↑(N + 1) * ∑ i ∈ Finset.range (N + 1), ∑ j ∈ Finset.range (N + 1), z ^ i * star (z ^ j); (helperForLemma_5_4_6_fejerPolynomial N) ↑x = D

Helper for Lemma 5.4.6: rewrite the weighted Fourier-coefficient sum for the Fejér kernel value into a normalized double geometric sum.

theorem helperForLemma_5_4_6_doubleGeomSum_eq_normSq_geomSum (N : ℕ) (z : ℂ) : have S := ∑ j ∈ Finset.range (N + 1), z ^ j; have D := 1 / ↑(N + 1) * ∑ i ∈ Finset.range (N + 1), ∑ j ∈ Finset.range (N + 1), z ^ i * star (z ^ j); D.re = 1 / (↑N + 1) * ‖S‖ ^ 2 ∧ D.im = 0

Helper for Lemma 5.4.6: the normalized double geometric sum equals the normalized squared geometric-sum norm, with vanishing imaginary part.

theorem helperForLemma_5_4_6_fejer_eval_eq_normSqGeometricSum (N : ℕ) (x : ℝ) : ((helperForLemma_5_4_6_fejerPolynomial N) ↑x).re = 1 / (↑N + 1) * ‖∑ j ∈ Finset.range (N + 1), Complex.exp (Complex.I * (2 * ↑Real.pi * ↑x)) ^ j‖ ^ 2 ∧ ((helperForLemma_5_4_6_fejerPolynomial N) ↑x).im = 0

Helper for Lemma 5.4.6: Fejér-kernel evaluation at a real point as a normalized squared geometric-sum norm, with vanishing imaginary part.

theorem helperForLemma_5_4_6_geomSum_norm_le_two_div_normExpSubOne (N : ℕ) (x : ℝ) (hx : Complex.exp (Complex.I * (2 * ↑Real.pi * ↑x)) ≠ 1) : ‖∑ j ∈ Finset.range (N + 1), Complex.exp (Complex.I * (2 * ↑Real.pi * ↑x)) ^ j‖ ≤ 2 / ‖Complex.exp (Complex.I * (2 * ↑Real.pi * ↑x)) - 1‖

Helper for Lemma 5.4.6: geometric-sum norm bound away from the resonance exp(2πix) = 1.

theorem helperForLemma_5_4_6_annulus_expSubOne_lowerBound {δ : ℝ} (hδ₀ : 0 < δ) (hδ₁ : δ < 1 / 2) : ∃ mδ > 0, ∀ (x : ℝ), δ ≤ |x| → |x| ≤ 1 - δ → mδ ≤ ‖Complex.exp (Complex.I * (2 * ↑Real.pi * ↑x)) - 1‖

Helper for Lemma 5.4.6: on the annulus δ ≤ |x| ≤ 1 - δ with 0 < δ < 1/2, the denominator ‖exp(2πix) - 1‖ is uniformly bounded below by a positive constant.

theorem helperForLemma_5_4_6_fejer_tailBound_from_formula {δ mδ : ℝ} (hmδ : 0 < mδ) (hLower : ∀ (x : ℝ), δ ≤ |x| → |x| ≤ 1 - δ → mδ ≤ ‖Complex.exp (Complex.I * (2 * ↑Real.pi * ↑x)) - 1‖) (N : ℕ) (x : ℝ) (hxδ : δ ≤ |x|) (hx1 : |x| ≤ 1 - δ) : ‖(helperForLemma_5_4_6_fejerPolynomial N) ↑x‖ ≤ 4 / mδ ^ 2 / (↑N + 1)

Helper for Lemma 5.4.6: combining the norm-square Fejér formula, geometric-sum denominator estimate, and annulus denominator lower bound gives the quantitative tail estimate.

theorem helperForLemma_5_4_6_fejer_real_nonneg_and_tailBound {δ : ℝ} (hδ₀ : 0 < δ) (hδ₁ : δ < 1 / 2) : (∀ (N : ℕ) (x : AddCircle 1), ((helperForLemma_5_4_6_fejerPolynomial N) x).im = 0 ∧ 0 ≤ ((helperForLemma_5_4_6_fejerPolynomial N) x).re) ∧ ∃ Cδ > 0, ∀ (N : ℕ) (x : ℝ), δ ≤ |x| → |x| ≤ 1 - δ → ‖(helperForLemma_5_4_6_fejerPolynomial N) ↑x‖ ≤ Cδ / (↑N + 1)

Helper for Lemma 5.4.6: Fejér kernels are pointwise real/nonnegative and satisfy uniform annulus decay ‖F_N(x)‖ ≤ Cδ/(N+1) when δ ≤ |x| ≤ 1-δ.

theorem helperForLemma_5_4_6_exists_fejerPeriodicApproximation (ε δ : ℝ) (hε : 0 < ε) (hδ₀ : 0 < δ) (hδ₁ : δ < 1 / 2) : ∃ (N : ℕ), IsPeriodicApproximationToIdentity ε δ (helperForLemma_5_4_6_fejerPolynomial N)

Helper for Lemma 5.4.6: quantitative Fejér-kernel concentration yields a periodic (ε, δ) approximation to the identity for some index.

theorem exists_trigonometricPolynomial_isPeriodicApproximationToIdentity (ε δ : ℝ) (hε : 0 < ε) (hδ₀ : 0 < δ) (hδ₁ : δ < 1 / 2) : ∃ (P : C(AddCircle 1, ℂ)), IsTrigonometricPolynomial P ∧ IsPeriodicApproximationToIdentity ε δ P

Lemma 5.4.6: for every ε > 0 and 0 < δ < 1/2, there exists a trigonometric polynomial P that is a periodic (ε, δ) approximation to the identity.