Bridge: inner product on EuclideanSpace ↔ dotProduct #
Inner product on EuclideanSpace ℝ (Fin n) equals dotProduct on the raw Fin n → ℝ
representation, when we embed via (WithLp.equiv 2 _).symm.
ONB construction for column span #
ONB construction for column span.
Given a matrix X, a vector θ*, and a support set S of size k,
there exists an orthonormal basis (Φ₁,...,Φᵣ) of the column span
span{Xⱼ : j ∈ S ∪ supp(θ*)} with:
r ≤ k + ‖θ*‖₀(dimension bound)- Isometry:
‖∑ aⱼΦⱼ‖² ≤ 1whenever‖a‖² ≤ 1
The proof uses stdOrthonormalBasis applied to the finite-dimensional
subspace spanned by the relevant column vectors.
ONB representability for column span.
Given a matrix X, a vector θ*, a support set S of size k, and θ supported on S,
if v = X·(θ-θ*) ≠ 0, then the ONB (Φ₁,...,Φᵣ) constructed by column_span_onb
can represent v/‖v‖: there exist coefficients a with dotProduct a a ≤ 1 such that
∑ aⱼΦⱼ = v / ‖v‖ component-wise.
The proof shows:
- v ∈ span{Xⱼ : j ∈ S ∪ supp(θ*)} (column-sum decomposition)
- v/‖v‖ has unit norm in the span
- ONB decomposition: coefficients from he.repr have ‖a‖ = ‖v/‖v‖‖ = 1
Subspace Theorem 1.19 bound #
Subspace Theorem 1.19 bound.
For a subspace W ⊆ ℝ^n of dimension r, if ε is a random vector whose projections onto unit vectors are sub-Gaussian(σ²), then: P(∃ unit u ∈ W, |ε·u| > t) ≤ 6^r · exp(-t²/(8σ²))
This follows from theorem_1_19_tail_bound_vec by identifying W with ℝ^r via an ONB.
The proof uses:
stdOrthonormalBasis ℝ Wto get an ONB of W indexed byFin (finrank ℝ W)- For each ONB vector b_j, the projection ε·b_j is sub-Gaussian(σ²)
- The supremum over unit vectors in W equals the supremum over unit coefficient vectors
- Apply
theorem_1_19_tail_bound_vecto the r-dimensional projected random vector
Theorem (ONB event containment step) [sorry'd].
For any S-supported θ with v = X(θ-θ*) ≠ 0, if 4⟨ε,v⟩² > ‖v‖²(2nτ²|θ|₀+t), then writing v = ‖v‖ · Σ aⱼ Φⱼ (ONB representation) with ‖a‖ ≤ 1, we get ⟨a/‖a‖, Φᵀε⟩ > √((t+2nτ²k)/4).
This follows from Cauchy-Schwarz ⟨ε,v⟩ = ‖v‖⟨ε, Σ aⱼ Φⱼ⟩ and monotonicity of the threshold. The book implicitly uses this in lines 1604-1610 of the proof. The full Lean proof requires extensive linear algebra infrastructure for ONB decompositions that is not available in Mathlib (in particular, representing arbitrary vectors in the column span as ONB linear combinations and connecting the Cauchy-Schwarz algebra to the set containment).
ONB event containment #
The book (lines 1600-1604) constructs an ONB Φ_{S,} for the column span span{X_j : j ∈ S ∪ supp(θ)} and uses it to reduce the supremum over parameter vectors to a supremum over the unit ball in ℝ^r.
The argument combines:
column_span_onb(proven above): constructs (r, Φ) with dimension bound and isometry- Event containment: the quadratic form event is contained in the ONB inner product event
The event containment step uses:
- For θ supported on S, X(θ-θ*) lies in span{X_j : j ∈ S ∪ supp(θ*)}
- Cauchy-Schwarz: 4⟨ε,v⟩² > ‖v‖²·C implies ⟨ε, v/‖v‖⟩ > √(C/4)
- The normalized vector v/‖v‖ is in the unit ball of the span, hence in the ONB image
ONB event containment.
Combines the ONB construction (column_span_onb) with the event containment step.
For any θ supported on S, the quadratic form violation event
4⟨ε,X(θ-θ*)⟩² > ‖X(θ-θ*)‖²·(2nτ²·l0norm(θ)+t) is contained in the ONB event
⟨∑ aⱼΦⱼ, ε⟩ > √((t+2nτ²k)/4) for some unit vector a in ℝ^r.
The key steps (not explicitly given in the book) are:
- v = X(θ-θ*) ∈ span{Xⱼ : j ∈ S ∪ supp(θ*)}, so v/‖v‖ = ∑ aⱼΦⱼ with ‖a‖=1
- 4⟨ε,v⟩² > ‖v‖²·(2nτ²·l0norm(θ)+t) implies ⟨ε,v/‖v‖⟩² > (2nτ²·l0norm(θ)+t)/4
- Since l0norm(θ) ≤ k (as supp(θ) ⊆ S with |S|=k), and in the book's formulation the supremum is taken over supp(θ)=S so l0norm(θ)=k, the threshold matches.
Theorem: Single-support-set concentration bound.
For a fixed support set S of size k, the probability that some θ with support
in S has 4⟨ε,X(θ-θ*)⟩² > ‖X(θ-θ*)‖²(2nτ²l0(θ)+t) is bounded by
6^(k + l0(θ*)) · exp(-t/(32σ²) - nτ²k/(16σ²)).
This uses subspace_thm119_bound applied to the ONB of the column span,
with threshold √((t+2nτ²k)/4).