Theorems · Theorem · complex analysis

Function.Periodic.tendsto_at_I_inf

∀ {h : ℝ} {f : ℂ → ℂ},
  0 < h →
    Function.Periodic f ↑h →
      (∀ᶠ (z : ℂ) in Filter.comap Complex.im Filter.atTop, DifferentiableAt ℂ f z) →
        (Filter.comap Complex.im Filter.atTop).BoundedAtFilter f →
          Filter.Tendsto f (Filter.comap Complex.im Filter.atTop) (nhds (Function.Periodic.cuspFunction h f 0))

If f is periodic, and holomorphic and bounded near I∞, then it tends to a limit at I∞, and this limit is the value of its cusp function at 0.

Defined in

Mathlib.Analysis.Complex.Periodic

Cited by

0 results in Mathlib

Foundations

Depth 289 from the axioms · uses propext, Classical.choice, Quot.sound