Ratios of sines and of hyperbolic sines at proportional arguments

For a fixed t ∈ [0, 1] this file compares sin (t * a) with sin a and sinh (t * b) with sinh b. The sine is concave on [0, π] and the hyperbolic sine is convex on [0, ∞), so t * sin a ≤ sin (t * a) for a ∈ [0, π] and sinh (t * b) ≤ t * sinh b for b ≥ 0. Moreover the ratio sin (t * a) / sin a increases with a on (0, π), while sinh (t * b) / sinh b decreases with b on (0, ∞).

These ratios are the distortion coefficients of the model spaces of constant curvature: up to rescaling, sin (t * a) / sin a compares the Jacobi field along a geodesic of a sphere at time t with its value at time 1, and sinh (t * b) / sinh b does the same in hyperbolic space. The monotonicity statements say that these comparisons grow with the curvature.

Main statements

• Real.strictConvexOn_sinh_Ici: sinh is strictly convex on [0, ∞).
• Real.mul_sin_le_sin_mul: t * sin a ≤ sin (t * a) for t ∈ [0, 1] and a ∈ [0, π].
• Real.sinh_mul_le_mul_sinh: sinh (t * b) ≤ t * sinh b for t ∈ [0, 1] and b ≥ 0.
• Real.monotoneOn_sin_mul_div_sin: a ↦ sin (t * a) / sin a is monotone on (0, π).
• Real.antitoneOn_sinh_mul_div_sinh: b ↦ sinh (t * b) / sinh b is antitone on (0, ∞).

theorem Real.strictConvexOn_sinh_Ici : StrictConvexOn ℝ (Set.Ici 0) sinh

The hyperbolic sine is strictly convex on [0, ∞).

theorem Real.mul_sin_le_sin_mul {t a : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (ha₀ : 0 ≤ a) (ha : a ≤ Real.pi) : t * sin a ≤ sin (t * a)

For t ∈ [0, 1] and a ∈ [0, π], t * sin a ≤ sin (t * a).

theorem Real.sinh_mul_le_mul_sinh {t b : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (hb : 0 ≤ b) : sinh (t * b) ≤ t * sinh b

For t ∈ [0, 1] and b ≥ 0, sinh (t * b) ≤ t * sinh b.

theorem Real.monotoneOn_sin_mul_div_sin {t : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) : MonotoneOn (fun (a : ℝ) => sin (t * a) / sin a) (Set.Ioo 0 Real.pi)

For t ∈ [0, 1], the ratio sin (t * a) / sin a is monotone in a on (0, π).

theorem Real.antitoneOn_sinh_mul_div_sinh {t : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) : AntitoneOn (fun (b : ℝ) => sinh (t * b) / sinh b) (Set.Ioi 0)

For t ∈ [0, 1], the ratio sinh (t * b) / sinh b is antitone in b on (0, ∞).