Better `Real.sin` bounds

Stream: Is there code for X?

[Aaron Liu]

I found docs#Real.sin_bound which gives a fourth-order remainder |x| ≤ 1 → |sin x - (x - x ^ 3 / 6)| ≤ |x| ^ 4 * (5 / 96), but this is not enough for what I want. I took a look at where this comes from, it comes from docs#Complex.exp_bound which is stated for an arbitrary amount of taylor series, which was then specialized to n := 4. Do we have any better bounds anywhere?

[Jireh Loreaux]

Using docs#Complex.exp_bound seems like a suboptimal way to achieve this bound, both in terms of the final result, and the method. I would have expected to see this using the tsum value for Real.sin, the fact that this alternates, and the fact that Real.sin (and its Taylor polynomials) are odd.

[Jireh Loreaux]

That is, using docs#Real.hasSum_sin, you should be able to show |Real.sin r - ∑ j ∈ Finset.range (n+1), (-1) ^ j * r ^ (2 * j + 1) / ↑(2 * j + 1)!| ≤ |r| ^ (2 * n + 3) / ↑(2 * n + 3)!.

[Jireh Loreaux]

Although I'm sad to realize we never did the generalization (of HasSum) described here: #mathlib4 > Conditionally convergent series @ 💬

[Geoffrey Irving]

I have arbitrary term bounds for sin and cos at

1. https://github.com/girving/interval/blob/2eb9470dd50eee13d892398f1758bc9c3cd783e7/Interval/Interval/Sincos.lean#L100
2. https://github.com/girving/interval/blob/2eb9470dd50eee13d892398f1758bc9c3cd783e7/Interval/Interval/Sincos.lean#L140

[Kim Morrison]

It would be great to get these up into Mathlib!

[Geoffrey Irving]

I've factored the bounds out of the interval file, as

https://github.com/girving/interval/blob/main/Interval/Misc/TrigBounds.lean

If you let me know (1) which parts of that file you'd like upstreamed and (2) where they should go, I can send a PR. I do think it would be nice to have Complex.sinc too.

I'm less sure about sinc_sqrt and cos_sqrt. The neat thing is that these are entire functions, and they are very useful for computations, but they're not very standard.

[Geoffrey Irving]

Didn't need the 0 < n condition for the sin bounds, actually: https://github.com/girving/interval/commit/11784e2dc5533fe340b9a1e6b56f3bf0aad454c5#diff-8f35b657e1c6f17ad17ea6e04edcc9e5ced1243fbe02e685e5fb4dcd48f90791

[Ruben Van de Velde]

Certainly the first 116 lines could go somewhere under Trigonometric. That seems like a good starting point

[Geoffrey Irving]

PR here: https://github.com/leanprover-community/mathlib4/pull/29355

[Ruben Van de Velde]

Thanks, commented