Removable singularities along a period lattice

Elementary analytic facts about functions that are only controlled off the lattice L.lattice of a period pair L:

• PeriodPair.countable_lattice, PeriodPair.eventually_notMem_lattice: the lattice is countable and avoided by a punctured neighbourhood of every point;
• PeriodPair.differentiable_of_periodic: a lattice-periodic function that is differentiable at 0 and off the lattice is entire.

theorem PeriodPair.countable_lattice (L : PeriodPair) : (↑L.lattice).Countable

The lattice of a period pair is countable.

theorem PeriodPair.eventually_notMem_lattice (L : PeriodPair) (l₀ : ℂ) : ∀ᶠ (u : ℂ) in nhdsWithin l₀ {l₀}ᶜ, u ∉ L.lattice

Every point has a punctured neighbourhood avoiding the lattice.

theorem PeriodPair.differentiable_of_periodic (L : PeriodPair) {H : ℂ → ℂ} (hper : ∀ w ∈ L.lattice, Function.Periodic H w) (h₀ : DifferentiableAt ℂ H 0) (hoff : ∀ x ∉ L.lattice, DifferentiableAt ℂ H x) : Differentiable ℂ H

A function that is periodic under every lattice vector, differentiable at 0 and differentiable off the lattice is differentiable everywhere.