feat(Analysis/Complex): periodic holo funcs factor through exponential

[loefflerd]

trafficstars

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.

---

These results will be used in a subsequent PR to define q-expansions for modular forms.

[github-actions[bot]]

PR summary adafb0df92

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.Complex.Periodic	1991

---

Declarations diff

+ abs_qParam + abs_qParam_lt_iff + boundedAtFilter_cuspFunction + cuspFunction + cuspFunction_eq_of_nonzero + cuspFunction_zero_eq_limUnder_nhds_ne + cuspFunction_zero_of_zero_at_inf + differentiableAt_cuspFunction + differentiableAt_cuspFunction_zero + eq_cuspFunction + eventually_differentiableAt_cuspFunction_nhds_ne_zero + exp_decay_of_zero_at_inf + im_invQParam + invQParam + invQParam_tendsto + log_exp_exists + qParam + qParam_left_inv_mod_period + qParam_right_inv + qParam_tendsto + tendsto_at_I_inf

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[CBirkbeck]

Ok it was easier to just push a change with new names, but if you don't agree then we can just revert the commit.

[CBirkbeck]

LGTM!

[MichaelStollBayreuth]

maintainer delegate

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by MichaelStollBayreuth.

[mathlib-bors[bot]]

:v: loefflerd can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[loefflerd]

Thanks Michael and Johan!

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style