Inner products in a star

Vectors are functions ι → ℝ with the dot product ∑ i, y i * x i. When unit vectors y j all have inner product at least κ with a common unit vector x, they are close to each other.

• le_inner_of_le_inner: two such vectors have inner product at least 4κ - 3.
• sum_inner_ordered_pairs_ge: for n such vectors and κ ≥ 0, the inner products over ordered pairs sum to at least n² κ² - n, since the sum of the vectors has squared norm at least (n κ)² by Cauchy–Schwarz.

Complexitylib.Algebraic.LowerBound.Cutwidth.Gaussian.Frontier.Arccos turns these bounds into a bound on the pairwise angles.

theorem Algebraic.Cutwidth.Gaussian.le_inner_of_le_inner {ι : Type} [Fintype ι] {x y y' : ι → ℝ} (hx : ∑ i : ι, x i ^ 2 = 1) (hy : ∑ i : ι, y i ^ 2 = 1) (hy' : ∑ i : ι, y' i ^ 2 = 1) {κ : ℝ} (hyx : κ ≤ ∑ i : ι, y i * x i) (hy'x : κ ≤ ∑ i : ι, y' i * x i) : 4 * κ - 3 ≤ ∑ i : ι, y i * y' i

Unit vectors close to a common unit vector are close to each other.

theorem Algebraic.Cutwidth.Gaussian.sum_inner_ordered_pairs_ge {ι J : Type} [Fintype ι] [DecidableEq J] {x : ι → ℝ} (hx : ∑ i : ι, x i ^ 2 = 1) (s : Finset J) (y : J → ι → ℝ) (hy : ∀ j ∈ s, ∑ i : ι, y j i ^ 2 = 1) {κ : ℝ} (hκ : 0 ≤ κ) (hyx : ∀ j ∈ s, κ ≤ ∑ i : ι, y j i * x i) : ↑s.card ^ 2 * κ ^ 2 - ↑s.card ≤ ∑ j ∈ s, ∑ j' ∈ s.erase j, ∑ i : ι, y j i * y j' i

Star inequality. If n unit vectors each have inner product at least κ ≥ 0 with a unit vector, the sum of their inner products over ordered pairs is at least n² κ² - n.