Vector discrepancy

DefinitionVector discrepancy#✓fully proved

For a real \(m \times n\) matrix \(A\), the vector discrepancy of \(A\) is the infimum, over all families \(u_1, \dots, u_n\) of unit vectors in the Euclidean space \(\mathbb{R}^n\), of \(\max_{1 \le i \le m} \lVert \sum_{j=1}^{n} A_{ij} u_j \rVert\) (taken to be \(0\) when \(m = 0\)), where \(\lVert \cdot \rVert\) is the Euclidean norm; it is an element of \([0, \infty]\).

def vectorDiscrepancy (A : Matrix (Fin m) (Fin n) ℝ) : ENNReal :=
  ⨅ u : {u : Fin n → EuclideanSpace ℝ (Fin n) // ∀ j, ‖u j‖ = 1},
    ENNReal.ofReal ‖fun i : Fin m => ∑ j, A i j • u.1 j‖

Used by 2

Used byStatement of Nikolov's bound on vector discrepancy · The vector discrepancy is attained

TheoremThe vector discrepancy is attained#✓fully proved

Let \(A\) be a real \(m \times n\) matrix with \(n \ge 1\). Then there are unit vectors \(u_1, \dots, u_n\) in the Euclidean space \(\mathbb{R}^n\) such that the vector discrepancy of \(A\) equals \(\max_{1 \le i \le m} \lVert \sum_{j=1}^{n} A_{ij} u_j \rVert\) (taken to be \(0\) when \(m = 0\)), where \(\lVert \cdot \rVert\) is the Euclidean norm.

theorem vectorDiscrepancy_attained (hn : 1 ≤ n)
    (A : Matrix (Fin m) (Fin n) ℝ) :
    ∃ u : Fin n → EuclideanSpace ℝ (Fin n), (∀ j, ‖u j‖ = 1) ∧
      vectorDiscrepancy A = ENNReal.ofReal ‖fun i : Fin m => ∑ j, A i j • u j‖

Uses 1

Statement usesVector discrepancy

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.