Periodicity of the derivative and the logarithmic derivative

Differentiation commutes with translation of the domain, so the Fréchet and the one-variable derivative of a periodic function are periodic with the same period, and hence so is the logarithmic derivative. All three statements are unconditional: fderiv, deriv, and with them logDeriv take their junk values at non-differentiable points, and the translation identities hold there too.

These extensions of Mathlib's periodicity API live in the root Function namespace as Periodic.*, so that hf.deriv and its analogues resolve by receiver notation. They remain protected so that opening Function.Periodic does not shadow deriv and logDeriv themselves.

Main declarations

• Function.Periodic.fderiv: the Fréchet derivative of a periodic function is periodic.
• Function.Periodic.deriv: the derivative of a periodic function is periodic.
• Function.Periodic.logDeriv: the logarithmic derivative of a periodic function is periodic.

theorem Function.Periodic.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {c : E} (hf : Periodic f c) : Periodic (fderiv 𝕜 f) c

The Fréchet derivative of a periodic function is periodic.

theorem Function.Periodic.deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {c : 𝕜} (hf : Periodic f c) : Periodic (deriv f) c

The derivative of a periodic function is periodic.

theorem Function.Periodic.logDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {c : 𝕜} (hf : Periodic f c) : Periodic (logDeriv f) c

The logarithmic derivative of a periodic function is periodic.