Angles within a spherical cap

Fix a unit vector x of a real inner product space and κ ≥ 0. The unit vectors y with κ ≤ ⟪y, x⟫ form the spherical cap of angular radius arccos κ around x. Vectors in such a cap are close to each other:

• InnerProductGeometry.two_mul_sq_sub_one_le_inner: two of them have inner product at least 2 κ ^ 2 - 1 = cos (2 arccos κ), by the triangle inequality for angles.
• InnerProductGeometry.le_sum_offDiag_inner: n of them have inner products summing, over the ordered pairs of distinct indices, to at least n ^ 2 κ ^ 2 - n. Indeed their sum S has ‖S‖ ≥ ⟪S, x⟫ ≥ n κ, and ‖S‖ ^ 2 is n plus that sum (norm_sum_sq_real).
• InnerProductGeometry.sum_offDiag_angle_le: if moreover κ ≥ √2 / 2, these inner products lie in [0, 1], where arccos is concave, so by Jensen's inequality the angles over the n (n - 1) ordered pairs sum to at most n (n - 1) arccos ((n κ ^ 2 - 1) / (n - 1)).

The last bound beats the pairwise bound 2 arccos κ on every angle: for n = 3 the average inner product is at least (3 κ ^ 2 - 1) / 2, which exceeds 2 κ ^ 2 - 1 by (1 - κ ^ 2) / 2.

Main results

• norm_sum_sq_real: the squared norm of a finite sum, expanded over the diagonal and the ordered pairs of distinct indices.
• InnerProductGeometry.two_mul_sq_sub_one_le_inner: the pairwise bound in a cap.
• InnerProductGeometry.le_sum_offDiag_inner: the bound on the sum of the pairwise inner products in a cap.
• InnerProductGeometry.sum_offDiag_angle_le: the bound on the sum of the pairwise angles in a cap.

theorem norm_sum_sq_real {V : Type u_1} {ι : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (s : Finset ι) (f : ι → V) : ‖∑ i ∈ s, f i‖ ^ 2 = ∑ i ∈ s, ‖f i‖ ^ 2 + ∑ p ∈ s.offDiag, inner ℝ (f p.1) (f p.2)

The squared norm of a finite sum is the sum of the squared norms plus the inner products over the ordered pairs of distinct indices.

theorem InnerProductGeometry.angle_eq_arccos_inner_of_norm_eq_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : angle x y = Real.arccos (inner ℝ x y)

The angle between unit vectors is the arccos of their inner product.

theorem InnerProductGeometry.two_mul_sq_sub_one_le_inner {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y z : V} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) (hz : ‖z‖ = 1) {κ : ℝ} (hκ : 0 ≤ κ) (hyx : κ ≤ inner ℝ y x) (hzx : κ ≤ inner ℝ z x) : 2 * κ ^ 2 - 1 ≤ inner ℝ y z

Two vectors in a cap. Two unit vectors whose inner products with a unit vector x are at least κ ≥ 0 have inner product at least 2 κ ^ 2 - 1: each makes an angle at most arccos κ with x, so they make an angle at most 2 arccos κ ≤ π with each other.

theorem InnerProductGeometry.le_sum_offDiag_inner {V : Type u_1} {ι : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} (hx : ‖x‖ = 1) {s : Finset ι} {y : ι → V} (hy : ∀ i ∈ s, ‖y i‖ = 1) {κ : ℝ} (hκ : 0 ≤ κ) (hyx : ∀ i ∈ s, κ ≤ inner ℝ (y i) x) : ↑s.card ^ 2 * κ ^ 2 - ↑s.card ≤ ∑ p ∈ s.offDiag, inner ℝ (y p.1) (y p.2)

Many vectors in a cap. If n unit vectors have inner products at least κ ≥ 0 with a unit vector, their inner products over the ordered pairs of distinct indices sum to at least n ^ 2 κ ^ 2 - n.

theorem InnerProductGeometry.sum_offDiag_angle_le {V : Type u_1} {ι : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} (hx : ‖x‖ = 1) {s : Finset ι} {y : ι → V} (hy : ∀ i ∈ s, ‖y i‖ = 1) {κ : ℝ} (hκ : √2 / 2 ≤ κ) (hyx : ∀ i ∈ s, κ ≤ inner ℝ (y i) x) : ∑ p ∈ s.offDiag, angle (y p.1) (y p.2) ≤ ↑s.card * (↑s.card - 1) * Real.arccos ((↑s.card * κ ^ 2 - 1) / (↑s.card - 1))

Angles in a cap. If n unit vectors have inner products at least κ ≥ √2 / 2 with a unit vector, the angles between them over the n (n - 1) ordered pairs of distinct indices sum to at most n (n - 1) arccos ((n κ ^ 2 - 1) / (n - 1)).