Proposition 3.12: Properties of Sobolev ellipsoids

This file formalizes Proposition 3.12 from the textbook.

The Sobolev ellipsoids enjoy the following properties:

(i) (Monotonicity) For any Q > 0, 0 < β' < β ⟹ Θ(β, Q) ⊆ Θ(β', Q). Larger smoothness parameter β gives a smaller Sobolev ellipsoid.

(ii) (Continuity) For any Q > 0, β > 1/2 ⟹ f is continuous. When β > 1/2, the Fourier coefficients are absolutely summable and the trigonometric series defines a continuous function.

The proof is left as an exercise (Problem 3.5) in the textbook. Reference: Book lines 2355–2366.

Main declarations

• Chapter3.prop_3_12: Combined statement of Proposition 3.12 (both parts)
• Chapter3.prop_3_12_monotone: Part (i) — monotonicity of Sobolev ellipsoids
• Chapter3.prop_3_12_continuous: Part (ii) — absolute summability and continuity

theorem Chapter3.sobolevCoeff_mono {β β' : ℝ} (hβ' : 0 < β') (hββ' : β' ≤ β) (j : ℕ) : sobolevCoeff β' j ≤ sobolevCoeff β j

Sobolev coefficient is monotone in β: for 0 < β' ≤ β, a_j(β') ≤ a_j(β).

theorem Chapter3.sobolev_ellipsoid_monotone {M : ℕ} {β β' Q : ℝ} (hβ' : 0 < β') (hββ' : β' < β) (_hQ : 0 < Q) : SobolevEllipsoid β Q M ⊆ SobolevEllipsoid β' Q M

Prop 3.12(i): Sobolev ellipsoid monotonicity — larger β gives smaller set.

theorem Chapter3.sobolev_summable {M : ℕ} {β Q : ℝ} (_hβ : 1 / 2 < β) (hQ : 0 < Q) (θ : Fin M → ℝ) (hθ : θ ∈ SobolevEllipsoid β Q M) : (∑ j : Fin M, if sobolevCoeff β (↑j + 1) = 0 then 0 else |θ j|) ≤ √Q * √(∑ j : Fin M, if sobolevCoeff β (↑j + 1) = 0 then 0 else 1 / sobolevCoeff β (↑j + 1) ^ 2)

Prop 3.12(ii): Cauchy-Schwarz bound for Sobolev ellipsoid members. For β > 1/2, Σ 1/j^{2β} converges, giving absolute summability.

theorem Chapter3.prop_3_12_monotone {M : ℕ} {β β' Q : ℝ} (hβ' : 0 < β') (hββ' : β' < β) (hQ : 0 < Q) : SobolevEllipsoid β Q M ⊆ SobolevEllipsoid β' Q M

Proposition 3.12(i) (Monotonicity of Sobolev ellipsoids). For 0 < β' < β, Θ(β, Q) ⊆ Θ(β', Q).

theorem Chapter3.prop_3_12_summable {M : ℕ} {β Q : ℝ} (hβ : 1 / 2 < β) (hQ : 0 < Q) (θ : Fin M → ℝ) (hθ : θ ∈ SobolevEllipsoid β Q M) : (∑ j : Fin M, if sobolevCoeff β (↑j + 1) = 0 then 0 else |θ j|) ≤ √Q * √(∑ j : Fin M, if sobolevCoeff β (↑j + 1) = 0 then 0 else 1 / sobolevCoeff β (↑j + 1) ^ 2)

Proposition 3.12(ii) (Cauchy-Schwarz summability bound). For β > 1/2, members of Θ(β, Q) satisfy Σ|θ_j| ≤ √Q · √(Σ 1/a_j²).

theorem Chapter3.sobolevCoeff_ge_rpow_shift {β : ℝ} (hβ : 0 < β) (j : ℕ) : ↑(j + 1) ^ β ≤ sobolevCoeff β (j + 2)

For j ≥ 0, sobolevCoeff β (j+2) ≥ (j+1)^β. This lower-bounds the Sobolev coefficient at shifted index, used for the inverse-square summability argument.

theorem Chapter3.sobolevCoeff_pos_shift {β : ℝ} (hβ : 0 < β) (j : ℕ) : 0 < sobolevCoeff β (j + 2)

sobolevCoeff β (j+2) is strictly positive for β > 0.

theorem Chapter3.prop_3_12_continuous {β Q : ℝ} (hβ : 1 / 2 < β) (hQ : 0 < Q) (θ : ℕ → ℝ) (hθ : ∀ (M : ℕ), ∑ j ∈ Finset.range M, sobolevCoeff β (j + 1) ^ 2 * θ j ^ 2 ≤ Q) : (Summable fun (j : ℕ) => ‖θ j‖) ∧ Continuous fun (x : ℝ) => ∑' (j : ℕ), θ j * trigBasis (j + 1) x

Proposition 3.12(ii) (Continuity of Sobolev functions). For β > 1/2 and Q > 0, if θ belongs to the infinite-dimensional Sobolev ellipsoid Θ(β, Q) (i.e., all partial sums Σ_{j<M} a_j² θ_j² ≤ Q), then the Fourier coefficients are absolutely summable and the trigonometric series f(x) = Σⱼ θⱼ φⱼ(x) defines a continuous function.

The proof sketch: Cauchy-Schwarz gives Σ|θⱼ| ≤ √Q · √(Σ 1/a_j²), which converges for β > 1/2 since Σ 1/j^{2β} < ∞. Absolute convergence of the Fourier series (with bounded basis functions) implies uniform convergence, hence the limit is continuous.

The proof is left as an exercise (Problem 3.5).

theorem Chapter3.prop_3_12 : (∀ {M : ℕ} {β β' Q : ℝ}, 0 < β' → β' < β → 0 < Q → SobolevEllipsoid β Q M ⊆ SobolevEllipsoid β' Q M) ∧ ∀ {β Q : ℝ}, 1 / 2 < β → 0 < Q → ∀ (θ : ℕ → ℝ), (∀ (M : ℕ), ∑ j ∈ Finset.range M, sobolevCoeff β (j + 1) ^ 2 * θ j ^ 2 ≤ Q) → (Summable fun (j : ℕ) => ‖θ j‖) ∧ Continuous fun (x : ℝ) => ∑' (j : ℕ), θ j * trigBasis (j + 1) x

Proposition 3.12 (Properties of Sobolev ellipsoids).

The Sobolev ellipsoids enjoy the following properties:

(i) (Monotonicity) For any Q > 0, 0 < β' < β ⟹ Θ(β, Q) ⊆ Θ(β', Q).

(ii) (Continuity) For any Q > 0, β > 1/2 implies that the Fourier coefficients are absolutely summable and the trigonometric series f(x) = Σⱼ θⱼ φⱼ(x) defines a continuous function.

This bundles both parts of Proposition 3.12 from the textbook. See prop_3_12_monotone for part (i) and prop_3_12_continuous for part (ii).