Trigonometric bounds and nonvanishing criteria

The sine of π / x is positive for real x > 1. The sine of π * x is nonzero for nonzero x ∈ (-1, 1), a criterion used to detect nonflat Schwarz–Christoffel turns.

For angles α, β > 0 and γ ≥ 0 with α + β + γ < π, the quotient (cos α cos β + cos γ) / (sin α sin β) is greater than 1; by the second hyperbolic law of cosines it is the hyperbolic cosine of the side opposite γ in a hyperbolic triangle with angles α, β, γ. These supply the positive sine factors and the hyperbolic scale in the matrix representations of triangle groups.

theorem TauCeti.sin_pi_mul_ne_zero_of_mem_Ioo_of_ne_zero {x : ℝ} (hx : x ∈ Set.Ioo (-1) 1) (hx0 : x ≠ 0) : Real.sin (Real.pi * x) ≠ 0

If x is nonzero and strictly between -1 and 1, then sin (π * x) is nonzero.

theorem TauCeti.sin_pi_div_pos {x : ℝ} (hx : 1 < x) : 0 < Real.sin (Real.pi / x)

For a real denominator greater than one, the sine of π / x is positive.

theorem TauCeti.one_lt_cos_mul_cos_add_cos_div_sin_mul_sin {α β γ : ℝ} (hα : 0 < α) (hβ : 0 < β) (hγ : 0 ≤ γ) (h : α + β + γ < Real.pi) : 1 < (Real.cos α * Real.cos β + Real.cos γ) / (Real.sin α * Real.sin β)

If α, β > 0, γ ≥ 0 and α + β + γ < π, then (cos α cos β + cos γ) / (sin α sin β) > 1. Indeed cos α cos β - sin α sin β = -cos (π - α - β), and cos (π - α - β) < cos γ because 0 ≤ γ < π - α - β ≤ π.

theorem TauCeti.exists_pos_cosh_mul_sin_mul_sin_eq {α β γ : ℝ} (hα : 0 < α) (hβ : 0 < β) (hγ : 0 ≤ γ) (h : α + β + γ < Real.pi) : ∃ (t : ℝ), 0 < t ∧ Real.cosh t * (Real.sin α * Real.sin β) = Real.cos α * Real.cos β + Real.cos γ

Positive angles with sum less than π determine a positive hyperbolic scale t for which cosh t * sin α * sin β = cos α * cos β + cos γ.