noncomputable def Chapter3.sobolevCoeff (β : ℝ) (j : ℕ) : ℝ

Sobolev coefficients (eq 3.9): a_j = j^β for even j, (j-1)^β for odd j

def Chapter3.SobolevEllipsoid (β Q : ℝ) (M : ℕ) : Set (Fin M → ℝ)

Sobolev ellipsoid Θ(β, Q) for finite-dimensional truncation: the set of θ ∈ ℝ^M with Σ_{j=1}^M a_j² θ_j² ≤ Q

theorem Chapter3.sobolevCoeff_nonneg {β : ℝ} (_hβ : 0 ≤ β) (j : ℕ) : 0 ≤ sobolevCoeff β j

Sobolev coefficient is nonneg for β ≥ 0

theorem Chapter3.sobolevCoeff_one {β : ℝ} (hβ : β ≠ 0) : sobolevCoeff β 1 = 0

a_1 = 0 for β ≠ 0 (since j=1 is odd, (1-1)^β = 0^β = 0)

theorem Chapter3.sobolevEllipsoid_nonempty {β Q : ℝ} {M : ℕ} (hQ : 0 ≤ Q) : (SobolevEllipsoid β Q M).Nonempty

Sobolev ellipsoid is nonempty (contains zero)

def Chapter3.SobolevClassFn (β : ℕ) (L : ℝ) : Set (ℝ → ℝ)

Definition 3.10 (Sobolev class W(β, L)). Fix β ∈ {1, 2, ...} and L > 0. The Sobolev class W(β, L) is the set of functions f : [0,1] → ℝ (modeled as f : ℝ → ℝ restricted to [0,1]) such that: • f ∈ L₂([0,1]), • f^(β-1) is absolutely continuous on [0,1], • ∫₀¹ (f^(β)(x))² dx ≤ L², • f^(j)(0) = f^(j)(1) for j = 0, ..., β-1 (periodic boundary conditions).

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

Fourier coefficients of the j-th derivative of f with respect to the trigonometric basis: s_k(j) = ∫₀¹ f^(j)(t) φ_k(t) dt. When j = 0 this gives the ordinary Fourier coefficients θ_k = s_k(0). (Book line 2307: "the Fourier coefficients {s_k(j)}_{k≥1}")

theorem Chapter3.derivFourierCoeff_zero (f : ℝ → ℝ) (k : ℕ) : derivFourierCoeff f 0 k = ∫ (x : ℝ) in Set.Icc 0 1, f x * trigBasis k x

The Fourier coefficients of f itself are derivFourierCoeff f 0.