Angle sums in a star: proofs

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

• arccos is concave on [0, 1], since its derivative -1 / √(1 - x²) is antitone on (0, 1).
• Jensen's inequality with uniform weights on a nonempty family, followed by antitonicity of arccos, bounds the arccos-sum of a family in [0, 1] whose arguments average at least x₀.
• In a star of three, every ordered-pair inner product lies in [4κ - 3, 1] ⊆ [0, 1], and the six of them sum to at least 9κ² - 3 by the star inequality.

theorem Algebraic.Cutwidth.Gaussian.Internal.concaveOn_arccos : ConcaveOn ℝ (Set.Icc 0 1) Real.arccos

arccos is concave on [0, 1].

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

A finite family of arguments in [0, 1] with average at least x₀ has arccos-sum at most the family size times arccos x₀.

theorem Algebraic.Cutwidth.Gaussian.Internal.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 arccos-sum over the six ordered pairs at most 6 arccos ((3 κ² - 1) / 2).