theorem sq_sum_abs_le' {ι : Type u_1} (S : Finset ι) (f : ι → ℝ) : (∑ j ∈ S, |f j|) ^ 2 ≤ ↑S.card * ∑ j ∈ S, f j ^ 2

theorem quad_form_identity' {n d : ℕ} (X : Matrix (Fin n) (Fin d) ℝ) (θ : Fin d → ℝ) (hn : 0 < ↑n) : 1 / ↑n * ∑ i : Fin n, (∑ j : Fin d, X i j * θ j) ^ 2 = ∑ j1 : Fin d, ∑ j2 : Fin d, θ j1 * ((X.transpose * X) j1 j2 / ↑n) * θ j2

theorem psd_restricted' {n d : ℕ} (X : Matrix (Fin n) (Fin d) ℝ) (θ : Fin d → ℝ) (hn : 0 < ↑n) (T : Finset (Fin d)) : 0 ≤ ∑ j1 ∈ T, ∑ j2 ∈ T, θ j1 * ((X.transpose * X) j1 j2 / ↑n) * θ j2

theorem sum_sum_const_mul_eq' {ι₁ : Type u_1} {ι₂ : Type u_2} (S₁ : Finset ι₁) (S₂ : Finset ι₂) (f : ι₁ → ℝ) (g : ι₂ → ℝ) (c : ℝ) : ∑ j1 ∈ S₁, ∑ j2 ∈ S₂, f j1 * c * g j2 = (c * ∑ j1 ∈ S₁, f j1) * ∑ j2 ∈ S₂, g j2

theorem lemma_2_17_core {n d : ℕ} {k : ℝ} (X : Matrix (Fin n) (Fin d) ℝ) (θ : Fin d → ℝ) (S : Finset (Fin d)) (hn : 0 < ↑n) (hk : 0 < k) (hSk : ↑S.card ≤ k) (hINC : ∀ (i j : Fin d), |(X.transpose * X) i j / ↑n - if i = j then 1 else 0| ≤ 1 / (14 * k)) (hcone : ∑ j ∈ Finset.univ \ S, |θ j| ≤ 3 * ∑ j ∈ S, |θ j|) : 1 / 2 * ∑ j ∈ S, θ j ^ 2 ≤ 1 / ↑n * ∑ i : Fin n, (∑ j : Fin d, X i j * θ j) ^ 2

theorem lemma_2_17_norm_equivalence {n d : ℕ} (hn : 0 < n) (X : Matrix (Fin n) (Fin d) ℝ) (k : ℕ) (hk : 0 < k) (hINC : AssumptionINC X k) (S : Finset (Fin d)) (hS : S.card ≤ k) (θ : Fin d → ℝ) (hcone : ∑ j ∈ Finset.univ \ S, |θ j| ≤ 3 * ∑ j ∈ S, |θ j|) : ∑ j ∈ S, θ j ^ 2 ≤ 2 * (1 / ↑n * X.mulVec θ ⬝ᵥ X.mulVec θ)

Lemma 2.17 (INC cone condition implies norm bound). Under INC(k), if S ⊆ {1,...,d} with |S| ≤ k and θ satisfies the cone condition |θ_{Sᶜ}|₁ ≤ 3|θ_S|₁, then |θ_S|₂² ≤ 2 · |Xθ|₂² / n.