Commit 2026-07-07 23:35 1082fe00

feat(Analysis): strengthen bounds for sin (#41094) This PR strengthens various bounds for Real.sin in mathlib. The statement Complex.sin_bound now has a quintic right hand side with a smaller constant. This bound is always better in the range where the theorem applies. The same is true for Real.sin_bound. Since these changes broke the proof of sin_pos_of_pos_of_le_one, I fixed and golfed this proof. Next sin_gt_sub_cube is given a tight constant, and its range of validity is extended, and the proof is the same length. A version for weak inequality, and a version with absolute value is also added.