Commit 2024-11-08 20:31 efb737da

View on Github →

feat(Analysis/Complex): periodic holo funcs factor through exponential (#18065) We show that a holomorphic function which is periodic with a real period h is given by f z = F (exp (2 * pi * I * z / h)) for some holomorphic F, and moreover, if f is bounded as Im z -> infty then F extends holomorphically to q = 0.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/Periodic.lean

added theorem abs_qParam

added theorem abs_qParam_lt_iff

added theorem boundedAtFilter_cuspFunction

added def cuspFunction

added theorem cuspFunction_eq_of_nonzero

added theorem cuspFunction_zero_eq_limUnder_nhds_ne

added theorem cuspFunction_zero_of_zero_at_inf

added theorem differentiableAt_cuspFunction

added theorem differentiableAt_cuspFunction_zero

added theorem eq_cuspFunction

added theorem eventually_differentiableAt_cuspFunction_nhds_ne_zero

added theorem exp_decay_of_zero_at_inf

added theorem im_invQParam

added def invQParam

added theorem invQParam_tendsto

added def qParam

added theorem qParam_left_inv_mod_period

added theorem qParam_right_inv

added theorem qParam_tendsto

added theorem tendsto_at_I_inf

Modified Mathlib/Analysis/SpecialFunctions/Complex/Log.lean

added theorem Complex.log_exp_exists