Inner products in a star: proofs

Vectors are functions ι → ℝ with the dot product ∑ i, y i * x i.

• Two unit vectors with inner product at least κ with a common unit vector satisfy ‖y - y'‖² ≤ 2 ‖y - x‖² + 2 ‖x - y'‖², which gives inner product at least 4κ - 3.
• For the sum S of the vectors y j, ‖S‖² is the family size plus the ordered-pair inner products, and Cauchy–Schwarz against the unit vector gives ‖S‖² ≥ (n κ)².

Inner products of unit vectors

theorem Algebraic.Cutwidth.Gaussian.Internal.inner_le_one {ι : Type} [Fintype ι] {y y' : ι → ℝ} (hy : ∑ i : ι, y i ^ 2 = 1) (hy' : ∑ i : ι, y' i ^ 2 = 1) : ∑ i : ι, y i * y' i ≤ 1

Cauchy–Schwarz for unit vectors: their inner product is at most one.

theorem Algebraic.Cutwidth.Gaussian.Internal.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.Internal.sum_sq_sum_eq {ι J : Type} [Fintype ι] [DecidableEq J] (s : Finset J) (y : J → ι → ℝ) (hy : ∀ j ∈ s, ∑ i : ι, y j i ^ 2 = 1) : ∑ i : ι, (∑ j ∈ s, y j i) ^ 2 = ↑s.card + ∑ j ∈ s, ∑ j' ∈ s.erase j, ∑ i : ι, y j i * y j' i

The squared norm of a sum of unit vectors is the family size plus the inner products over ordered pairs.

theorem Algebraic.Cutwidth.Gaussian.Internal.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.