interval arithmetic

Stream: mathlib4

[Kim Morrison]

We're gearing up for interval arithmetic, and I'd like to provide soon some examples of what user extensibility might look like, i.e. theorems explaining how to propagate intervals through functions defined in Mathlib (between types defined in Mathlib!). I won't post about these today, but could I just ask for some quick review on some PRs that will make the examples go more smoothly?

[Kim Morrison]

feat: monotone helper lemmas for sin/cos #29021

[Kim Morrison]

chore: add fun_prop for ContDiff to trig functions #29022

[Kim Morrison]

feat: lemmas about iterated derivatives of trig functions #29023

[Kim Morrison]

feat: lemmas about iterated derivatives within real intervals #29024

[Kim Morrison]

chore: add @[simp] to PolynomialModule.eval_smul #29026