Calculus on the circle

Stream: maths

[Oliver Nash]

For one-dimensional domains, derivatives are just values. Because this special case is so important, we have a dedicated API for it. E.g., docs#deriv essentially specialises docs#fderiv to the case E = 𝕜.

However there is arguably one more important special case for which we do not have a dedicated API, namely the circle. It would be pretty easy to create one, starting perhaps like this:

import analysis.normed.group.add_circle
import analysis.calculus.deriv

noncomputable theory

variables {F : Type*} [normed_add_comm_group F] [normed_space ℝ F] {p : ℝ}

lemma add_circle.exists_rep (x : add_circle p) :
  ∃ (y : ℝ), (y : add_circle p) = x :=
@quotient.exists_rep ℝ (quotient_add_group.left_rel $ add_subgroup.zmultiples p) x

def has_cderiv_at (f : add_circle p → F) (f' : F) (x : add_circle p) : Prop :=
has_deriv_at (f ∘ coe) f' (classical.some $ add_circle.exists_rep x)

def cderiv (f : add_circle p → F) (x : add_circle p) : F :=
deriv (f ∘ coe) (classical.some $ add_circle.exists_rep x)

[Oliver Nash]

I just spent a few minutes considering whether such an API should be built and I decided no because the gap between cderiv (defined above) and docs#deriv is much smaller than between docs#deriv and docs#fderiv.

[Heather Macbeth]

There's also manifold-differentiability -- once we get around to putting a manifold structure on free quotients by discrete groups, which shouldn't be too bad.

[Oliver Nash]

Still, I thought I'd make this remark publicly in case anyone else had thoughts on the matter. The circle does come up a lot (Fourier series, Cauchy integrals) and it would be handy to have something like this.

[Oliver Nash]

You're too fast for me: treating it as a manifold was to be my last remark.