Theorems · Theorem · complex analysis

Function.Periodic.eventually_differentiableAt_cuspFunction_nhds_ne_zero

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

Defined in

Mathlib.Analysis.Complex.Periodic

Cited by

1 results in Mathlib

Foundations

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