noncomputable def Chapter3.haarMother (x : ℝ) : ℝ

The Haar mother wavelet: 1 on [0, 1/2), −1 on [1/2, 1], 0 elsewhere.

noncomputable def Chapter3.haarWavelet (j k : ℤ) (x : ℝ) : ℝ

The Haar wavelet family ψ_{jk}(x) = 2^{j/2} ψ(2^j x − k).

noncomputable def Chapter3.waveletCoeff (g : ℝ → ℝ) (j k : ℤ) : ℝ

Wavelet coefficient θ_{jk} = ∫₀¹ g(x) ψ_{jk}(x) dx.

theorem Chapter3.haarMother_stronglyMeasurable : MeasureTheory.StronglyMeasurable haarMother

theorem Chapter3.haarMother_intervalIntegrable (a b : ℝ) : IntervalIntegrable haarMother MeasureTheory.volume a b

theorem Chapter3.haarMother_bounded (x : ℝ) : |haarMother x| ≤ 1

The Haar mother wavelet is bounded: |ψ(x)| ≤ 1 for all x.

theorem Chapter3.haar_ae_first : ∀ᵐ (x : ℝ), x ∈ Set.uIoc 0 (1 / 2) → haarMother x = 1

theorem Chapter3.haarMother_integral_zero : ∫ (x : ℝ) in 0..1, haarMother x = 0

The Haar mother wavelet integrates to zero over [0, 1].