Commit 2025-10-23 17:08 0a19b1f2

View on Github →

feat: sharp bounds for ‖exp (I * x) - 1‖ when x is real (#27252) From Carleson

Estimated changes

Modified Mathlib/Analysis/Complex/Trigonometric.lean

added theorem Complex.enorm_exp_I_mul_ofReal

added theorem Complex.enorm_exp_ofReal_mul_I

added theorem Complex.nnnorm_exp_I_mul_ofReal

added theorem Complex.nnnorm_exp_ofReal_mul_I

added theorem Complex.norm_exp_I_mul_ofReal

added theorem Complex.norm_exp_I_mul_ofReal_sub_one

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

added theorem Real.enorm_exp_I_mul_ofReal_sub_one_le

added theorem Real.nnnorm_exp_I_mul_ofReal_sub_one_le

added theorem Real.norm_exp_I_mul_ofReal_sub_one_le