Angles in a star

Vectors are functions ι → ℝ with the dot product ∑ i, y i * x i, and the angle between two unit vectors is the arccos of their inner product. A star is a family of unit vectors y j each having inner product at least κ with a common unit vector x. The members of a star are close to each other:

• le_inner_of_le_inner: two of them have inner product at least 4κ - 3, by expanding ‖y - 2x + y'‖ ^ 2 ≥ 0.
• sum_inner_ordered_pairs_ge: if there are n of them and κ ≥ 0, their inner products over ordered pairs sum to at least n ^ 2 κ ^ 2 - n. Indeed their sum S has squared norm n plus that sum, and ‖S‖ ≥ ⟨S, x⟩ ≥ n κ by Cauchy-Schwarz.

Angles are then bounded by concavity:

• sum_arccos_le: arccos is antitone, and concave on [0, 1] since its derivative -1 / √(1 - x ^ 2) is antitone there. By Jensen's inequality, a family of arguments in [0, 1] with average at least x₀ has arccos-sum at most the family size times arccos x₀.
• sum_arccos_star_le: in a star of three with κ ≥ 7/8, the six ordered-pair inner products lie in [4κ - 3, 1] ⊆ [0, 1] and sum to at least 9 κ ^ 2 - 3, so the six angles sum to at most 6 arccos ((3 κ ^ 2 - 1) / 2).

Inner products in a star

theorem Complexity.Frontier.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 Complexity.Frontier.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 ^ 2 κ ^ 2 - n.

Angles in a star

theorem Complexity.Frontier.Gaussian.sum_arccos_le {J : Type} (s : Finset J) (x : J → ℝ) {x₀ : ℝ} (hx : ∀ j ∈ s, 0 ≤ x j ∧ x j ≤ 1) (hsum : ↑s.card * x₀ ≤ ∑ j ∈ s, x j) : ∑ j ∈ s, Real.arccos (x j) ≤ ↑s.card * Real.arccos x₀

Concavity bound for arccos. arccos is concave on [0, 1] and antitone, so a finite family of arguments in that interval with average at least x₀ has arccos-sum at most the family size times arccos x₀.

theorem Complexity.Frontier.Gaussian.sum_arccos_star_le {ι J : Type} [Fintype ι] [DecidableEq J] {x : ι → ℝ} (hx : ∑ i : ι, x i ^ 2 = 1) (s : Finset J) (hs : s.card = 3) (y : J → ι → ℝ) (hy : ∀ j ∈ s, ∑ i : ι, y j i ^ 2 = 1) {κ : ℝ} (hκ : 7 / 8 ≤ κ) (hyx : ∀ j ∈ s, κ ≤ ∑ i : ι, y j i * x i) : ∑ j ∈ s, ∑ j' ∈ s.erase j, Real.arccos (∑ i : ι, y j i * y j' i) ≤ 6 * Real.arccos ((3 * κ ^ 2 - 1) / 2)

Angles in a star of three. Three unit vectors with inner product at least κ ≥ 7/8 with a unit vector have pairwise angles summing, over the six ordered pairs, to at most 6 arccos ((3 κ ^ 2 - 1) / 2).