Commit 2025-01-20 01:43 f09f967a

feat: inequalities on complex exponentials (#20844) Two inequalities on complex exponentials:

abs (cexp x - ∑ m ∈ range n, x ^ m / m.factorial)
    ≤ Real.exp (abs x) - ∑ m ∈ range n, (abs x) ^ m / m.factorial
abs (cexp x - ∑ m ∈ range n, x ^ m / m.factorial) ≤ abs x ^ n * Real.exp (abs x)