Problem 2.4: Weak ℓ_q balls and approximation bounds

From Rigollet Chapter 2, Problem 2.4.

A vector θ ∈ ℝᵈ is in a weak ℓ_q ball of radius R if its decreasing rearrangement satisfies |θ_{[j]}| ≤ R · j^{-1/q}. The weak ℓ_q norm is defined as |θ|{wℓ_q} = max{1 ≤ j ≤ d} j^{1/q} |θ_{[j]}|.

Part (b): |θ|_{wℓ_q} ≤ |θ|_q.

structure IsDecreasingRearrangement {d : ℕ} (θ a : Fin d → ℝ) : Prop

A decreasing rearrangement of (fun i => |θ i|): a function a : Fin d → ℝ that gives the same multiset of values as (fun i => |θ i|) and is antitone (nonincreasing). The index convention is 0-based: a ⟨0, _⟩ is the largest.

• nonneg (j : Fin d) : 0 ≤ a j

  Each value is nonneg

• antitone : Antitone a

  The sequence is nonincreasing

• multiset_eq : Multiset.map a Finset.univ.val = Multiset.map (fun (i : Fin d) => |θ i|) Finset.univ.val

  It is a rearrangement of |θ ·| : same multiset of values

noncomputable def weakLqNorm {d : ℕ} [NeZero d] (q : ℝ) (a : Fin d → ℝ) : ℝ

Weak ℓ_q norm: ‖θ‖_{wℓ_q} = max_{1 ≤ j ≤ d} j^{1/q} · |θ_{[j]}| where a is the decreasing rearrangement (0-indexed, so j.val + 1 gives the 1-based index used in the mathematical definition).

noncomputable def strongLqNorm {d : ℕ} (q : ℝ) (θ : Fin d → ℝ) : ℝ

Strong ℓ_q norm: ‖θ‖_q = (∑ᵢ |θᵢ|^q)^{1/q}.

def InWeakLqBall {d : ℕ} (a : Fin d → ℝ) (q R : ℝ) : Prop

Membership in a weak ℓ_q ball of radius R: the j-th largest absolute value of θ is at most R · j^{-1/q}. Equivalently, weakLqNorm q a ≤ R.

theorem sum_comp_eq_of_multiset_map_eq {d : ℕ} (a b : Fin d → ℝ) (h : Multiset.map a Finset.univ.val = Multiset.map b Finset.univ.val) (f : ℝ → ℝ) : ∑ i : Fin d, f (a i) = ∑ i : Fin d, f (b i)

Helper: a rearrangement preserves sums under any function.

theorem problem_2_4b_weak_le_strong {d : ℕ} (hd : NeZero d) (θ a : Fin d → ℝ) (ha : IsDecreasingRearrangement θ a) (q : ℝ) (hq : 0 < q) : weakLqNorm q a ≤ strongLqNorm q θ

Problem 2.4(b). The weak ℓ_q norm is bounded by the strong ℓ_q norm: ‖θ‖_{wℓ_q} ≤ ‖θ‖_q, i.e., max_{j} (j+1)^{1/q} · a(j) ≤ (∑ᵢ |θᵢ|^q)^{1/q}.

The proof uses the fact that since a is the decreasing rearrangement, j · a(j)^q ≤ ∑ᵢ |θᵢ|^q for each j, so (j+1)^{1/q} · a(j) ≤ (∑ᵢ |θᵢ|^q)^{1/q}.