Commit 2024-09-01 01:42 63cced2a

View on Github →

chore(Analysis/SpecialFunctions): deduplicate and golf trig bounds (#16275) Remove the duplication of trig lemmas, introduced in a previous PR. Golf existing trig bounds. Add further bounds. Make the names more consistent throughout.

Estimated changes

added theorem Real.abs_sin_le_abs
added theorem Real.abs_sin_lt_abs
added theorem Real.le_sin_mul
added theorem Real.lt_sin_mul
added theorem Real.mul_le_sin
added theorem Real.mul_lt_sin
added theorem Real.sin_le_mul
added theorem Real.sin_sq_le_sq
added theorem Real.sin_sq_lt_sq
deleted theorem Real.le_sin_mul
deleted theorem Real.lt_sin_mul
deleted theorem Real.mul_le_sin
deleted theorem Real.mul_lt_sin