Commit 2024-03-02 14:20 5112b8d8

View on Github →

feat: Linear and quadratic bounds on sin and cos (#10525) ... including Jordan's inequality: 2 / π * x ≤ sin x for 0 ≤ x ≤ π / 2 From LeanAPAP

Estimated changes

Modified Mathlib/Analysis/Calculus/MeanValue.lean

deleted theorem StrictAntiOn_of_hasDerivWithinAt_pos

deleted theorem StrictMonoOn_of_hasDerivWithinAt_pos

added theorem strictAntiOn_of_hasDerivWithinAt_neg

added theorem strictAnti_of_hasDerivAt_neg

deleted theorem strictAnti_of_hasDerivAt_pos

added theorem strictMonoOn_of_hasDerivWithinAt_pos

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean

added theorem Real.cos_quadratic_upper_bound

added theorem Real.le_sin

added theorem Real.lt_sin

added theorem Real.one_sub_sq_div_two_le_cos

added theorem Real.one_sub_two_div_pi_mul_le_cos

added theorem Real.sin_le

added theorem Real.sin_le_two_div_pi_mul

modified theorem Real.sin_lt

added theorem Real.two_div_pi_mul_le_sin