Physlib.Mathematics.Trigonometry.SinSq

Strict bounds on the square of the sine

This file may eventually be upstreamed to Mathlib.

i. Overview

Mathlib bounds the square of the sine by `sin x ^ 2 ≤ 1` for every real `x` (`Real.sin_sq_le_one`), with equality exactly at the odd multiples of `π / 2`. This file records the strict form of that bound, `sin x ^ 2 < 1` on the open interval `|x| < π / 2`, where the cosine is positive and `1 - sin² x = cos² x`, together with its half-angle form `sin (θ / 2) ^ 2 < 1` for `|θ| < π`.

Physlib uses the half-angle form for the simple pendulum: the parameter `sin² (θ₀ / 2)` of the period formula lies in the domain `m < 1` of the complete elliptic integral `Real.completeEllipticK` for every libration amplitude `|θ₀| < π`.

ii. Key results

`Real.sin_sq_lt_one` : `sin x ^ 2 < 1` for `|x| < π / 2`.
`Real.sin_half_sq_lt_one` : `sin (θ / 2) ^ 2 < 1` for `|θ| < π`.

iii. Table of contents

A. Strict bounds on the square of the sine

iv. References

- Landau & Lifshitz, Mechanics, 3rd ed., §11, Problem 1 (the pendulum period, whose parameter is `sin² (θ₀ / 2)`).

A. Strict bounds on the square of the sine

On `|x| < π / 2` the cosine is positive, so `1 - sin² x = cos² x` is positive; the half-angle form follows by applying this at `x = θ / 2`.

2 declarations

theorem

$\sin^2 x < 1$ for $|x| < \frac{\pi}{2}$

#sin_sq_lt_one

For any real number $x$ , if the absolute value of $x$ satisfies $|x| < \frac{\pi}{2}$ , then the square of its sine satisfies $\sin^2 x < 1$ .

theorem

$\sin^2(\theta/2) < 1$ for $|\theta| < \pi$

#sin_half_sq_lt_one

For any real number $\theta$ such that $|\theta| < \pi$ , the square of the sine of the half-angle is strictly less than $1$ , i.e., $\sin^2(\theta / 2) < 1$ .