The half-angle formula and concavity of arccos

For -1 < x, the angle θ = arccos x satisfies tan (θ / 2) = √(1 - x) / √(1 + x), so arccos x = 2 arctan (√(1 - x) / √(1 + x)) (Real.arccos_eq_two_mul_arctan). The derivative -1 / √(1 - x ^ 2) of arccos is strictly decreasing on (0, 1), so arccos is strictly concave on [0, 1] (strictConcaveOn_arccos_Icc). By Jensen's inequality, arguments in [0, 1] with average at least x₀ have arccos-sum at most their number times arccos x₀ (Real.sum_arccos_le_card_mul_arccos).

Main results

• Real.arccos_eq_two_mul_arctan: the half-angle formula for arccos.
• strictConcaveOn_arccos_Icc: arccos is strictly concave on [0, 1].
• Real.sum_arccos_le_card_mul_arccos: Jensen's inequality for arccos on [0, 1].

theorem Real.arccos_eq_two_mul_arctan {x : ℝ} (hx : -1 < x) : arccos x = 2 * arctan (√(1 - x) / √(1 + x))

The half-angle formula for arccos: arccos x = 2 arctan (√(1 - x) / √(1 + x)) for -1 < x. For 1 ≤ x both sides vanish.

theorem strictConcaveOn_arccos_Icc : StrictConcaveOn ℝ (Set.Icc 0 1) Real.arccos

arccos is strictly concave on [0, 1]: its derivative -1 / √(1 - x ^ 2) is strictly decreasing on (0, 1).

theorem Real.sum_arccos_le_card_mul_arccos {ι : Type u_1} (s : Finset ι) {x : ι → ℝ} {x₀ : ℝ} (hx : ∀ i ∈ s, x i ∈ Set.Icc 0 1) (hsum : ↑s.card * x₀ ≤ ∑ i ∈ s, x i) : ∑ i ∈ s, arccos (x i) ≤ ↑s.card * arccos x₀

Jensen's inequality for arccos. If finitely many arguments in [0, 1] have average at least x₀, their arccos-sum is at most their number times arccos x₀.