noncomputable def Chapter3.trigBasis (j : ℕ) (x : ℝ) : ℝ

Trigonometric basis of L₂([0,1]). φ₁ ≡ 1, φ_{2k}(x) = √2 cos(2πkx), φ_{2k+1}(x) = √2 sin(2πkx) for k ≥ 1. Index j = 0 is unused (returns 0).

noncomputable def Chapter3.fourierCoeff (f : ℝ → ℝ) (j : ℕ) : ℝ

Fourier coefficient: θ_j* = ∫₀¹ f(x) φ_j(x) dx

theorem Chapter3.trigBasis_one (x : ℝ) : trigBasis 1 x = 1

The first basis function is the constant 1.

theorem Chapter3.trigBasis_bounded (j : ℕ) (x : ℝ) : |trigBasis j x| ≤ √2

Every trigonometric basis function is bounded by √2 in absolute value.