noncomputable def trigBasis : ℕ → ℝ → ℝ

The trigonometric basis of L₂([0,1]) (Example 3.8). φ₁(x) = 1, φ_{2k}(x) = √2 cos(2πkx), φ_{2k+1}(x) = √2 sin(2πkx) for k = 1, 2, … and x ∈ [0,1].

noncomputable def haarMother (x : ℝ) : ℝ

The Haar mother wavelet (Example 3.9). ψ(x) = 1 for 0 ≤ x < 1/2, ψ(x) = -1 for 1/2 ≤ x < 1, 0 otherwise.

noncomputable def haarSystem (j k : ℤ) (x : ℝ) : ℝ

The Haar wavelet system: ψ_{j,k}(x) = 2^{j/2} · ψ(2ʲx − k).

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

theorem trigBasis_of_ge_two (j : ℕ) (hj : 2 ≤ j) (x : ℝ) : trigBasis j x = if j % 2 = 0 then √2 * Real.cos (2 * Real.pi * ↑(j / 2) * x) else √2 * Real.sin (2 * Real.pi * ↑((j - 1) / 2) * x)

theorem trigBasis_orthonormal (j k : ℕ) (hj : 0 < j) (hk : 0 < k) : ∫ (x : ℝ) in 0..1, trigBasis j x * trigBasis k x = if j = k then 1 else 0

Problem 3.4 (Part 1) — Trigonometric basis is orthonormal in L₂([0,1]).

Rigollet, High-Dimensional Statistics, Problem 3.4 (line 2582).

The trigonometric basis (Example 3.8) is defined by φ₁(x) = 1, φ_{2k}(x) = √2 cos(2πkx), φ_{2k+1}(x) = √2 sin(2πkx) for k = 1, 2, … . Show that it forms an orthonormal system of L₂([0,1]): ∫₀¹ φⱼ(x) · φₖ(x) dx = δⱼₖ for all j, k ≥ 1.

The proof uses standard trigonometric product-to-sum identities (cos α cos β, sin α sin β, cos α sin β) together with the fact that ∫₀¹ cos(2πmx) dx = 0 and ∫₀¹ sin(2πmx) dx = 0 for any integer m ≠ 0.

theorem haarSystem_orthonormal (j j' k k' : ℤ) (hj : 0 ≤ j) (hj' : 0 ≤ j') (hk : 0 ≤ k ∧ k < 2 ^ j.toNat) (hk' : 0 ≤ k' ∧ k' < 2 ^ j'.toNat) : ∫ (x : ℝ) in 0..1, haarSystem j k x * haarSystem j' k' x = if j = j' ∧ k = k' then 1 else 0

Problem 3.4 (Part 2) — Haar system is orthonormal in L₂([0,1]).

Rigollet, High-Dimensional Statistics, Problem 3.4 (line 2582).

The Haar wavelet system (Example 3.9) is defined by ψ_{j,k}(x) = 2^{j/2} ψ(2ʲx − k) where ψ is the Haar mother wavelet (1 on [0,1/2), −1 on [1/2,1), 0 elsewhere). Show that it forms an orthonormal system of L₂([0,1]): ∫₀¹ ψ_{j,k}(x) · ψ_{j',k'}(x) dx = δ_{(j,k),(j',k')}.

When j = j', the supports of ψ_{j,k} and ψ_{j,k'} are disjoint for k ≠ k'. When j ≠ j' (say j < j'), the finer wavelet ψ_{j',k'} is constant on each half of the support of ψ_{j,k}, so the integral telescopes to zero.