Assumption ORT

Assumption ORT. The design matrix satisfies $$\frac{\mathbb{X}^\top \mathbb{X}}{n} = I_d,$$ where $I_d$ denotes the identity matrix of $\mathbb{R}^d$.

This is formalized as a structure on a real matrix X : Matrix (Fin n) (Fin d) ℝ. The book's condition X^T X / n = I_d is equivalent to X^T X = n • I_d, which is the form used here to avoid division in the matrix ring.

structure OrthogonalDesign.AssumptionORT {n d : ℕ} (X : Matrix (Fin n) (Fin d) ℝ) : Prop

Assumption ORT: The design matrix X satisfies Xᵀ X = n • Iₐ.

This is equivalent to the book's formulation Xᵀ X / n = Iₐ, restated without division to work cleanly in the matrix semiring. Concretely, it means the columns of X are orthogonal in ℝⁿ and each has squared norm n.

• ortho_condition : X.transpose * X = n • 1