Taylor series with remainder for sin and cos

Stream: Is there code for X?

[Geoffrey Irving]

Do we have docs#Real.exp_bound (Taylor series with remainder) for sin and cos? It seems like mathlib jumps directly from the power series for exp to power series for sin and cos, but as a result we don’t need the remainder bound (which I need).

[Gareth Ma]

I can't find anything with leansearch, so it's safe to say no

[Gareth Ma]

Irrelevant note, is Real.exp_approx_end a duplicate of Real.exp_bound?