Commit 2025-08-27 13:41 ee1b32ba

View on Github →

feat: lemmas about iterated derivatives of trig functions (#29023)

Estimated changes

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

added theorem Complex.differentiable_iteratedDeriv_cos

added theorem Complex.differentiable_iteratedDeriv_cosh

added theorem Complex.differentiable_iteratedDeriv_sin

added theorem Complex.differentiable_iteratedDeriv_sinh

added theorem Complex.iteratedDeriv_add_one_cos

added theorem Complex.iteratedDeriv_add_one_cosh

added theorem Complex.iteratedDeriv_add_one_sin

added theorem Complex.iteratedDeriv_add_one_sinh

added theorem Complex.iteratedDeriv_even_cos

added theorem Complex.iteratedDeriv_even_cosh

added theorem Complex.iteratedDeriv_even_sin

added theorem Complex.iteratedDeriv_even_sinh

added theorem Complex.iteratedDeriv_odd_cos

added theorem Complex.iteratedDeriv_odd_cosh

added theorem Complex.iteratedDeriv_odd_sin

added theorem Complex.iteratedDeriv_odd_sinh

added theorem Real.abs_iteratedDeriv_cos_le_one

added theorem Real.abs_iteratedDeriv_sin_le_one

added theorem Real.differentiable_iteratedDeriv_cos

added theorem Real.differentiable_iteratedDeriv_cosh

added theorem Real.differentiable_iteratedDeriv_sin

added theorem Real.differentiable_iteratedDeriv_sinh

added theorem Real.iteratedDeriv_add_one_cos

added theorem Real.iteratedDeriv_add_one_cosh

added theorem Real.iteratedDeriv_add_one_sin

added theorem Real.iteratedDeriv_add_one_sinh

added theorem Real.iteratedDeriv_even_cos

added theorem Real.iteratedDeriv_even_cosh

added theorem Real.iteratedDeriv_even_sin

added theorem Real.iteratedDeriv_even_sinh

added theorem Real.iteratedDeriv_odd_cos

added theorem Real.iteratedDeriv_odd_cosh

added theorem Real.iteratedDeriv_odd_sin

added theorem Real.iteratedDeriv_odd_sinh