The local parameter under translation, period rescaling, and differentiation

Identities for the local parameter 𝕢 h z = exp (2 π I z / h) at a cusp: translating the argument multiplies by an exponential, the m-th power of the local parameter at period m * h is the local parameter at period h, the values at the integer offsets b < p satisfy the roots-of-unity orthogonality relation, the parameter differentiates to itself times 2πi/h, and the logarithmic derivative of any periodic function of nonzero width h factors through its cusp function along the parameter.

Main declarations

• TauCeti.Periodic.qParam_sub: 𝕢 h (z - j) = 𝕢 h z * exp (-2 π I j / h).
• TauCeti.Periodic.qParam_nat_mul_pow: 𝕢 (m * h) z ^ m = 𝕢 h z for m ≠ 0.
• TauCeti.Periodic.sum_qParam_natCast_pow: the roots-of-unity orthogonality relation ∑_{b < p} 𝕢 p b ^ m = if p ∣ m then p else 0.
• TauCeti.Periodic.hasDerivAt_qParam (with deriv_qParam): the q-parameter differentiates to itself times 2πi/h.
• TauCeti.Periodic.logDeriv_eq_logDeriv_cuspFunction_mul_deriv_qParam: the chain rule for the logarithmic derivative of a periodic function of nonzero width through its cusp function.

References

• Mathlib PR #39083 (Chris Birkbeck) — the upstream draft this file ports onto the current Mathlib pin.

theorem TauCeti.Periodic.qParam_sub {h : ℝ} (z j : ℂ) : Function.Periodic.qParam h (z - j) = Function.Periodic.qParam h z * Complex.exp (-2 * ↑Real.pi * Complex.I * j / ↑h)

Translation by j in the argument of qParam corresponds to multiplication by exp (-2 π I j / h).

theorem TauCeti.Periodic.qParam_nat_mul_pow {h : ℝ} {m : ℕ} (hm : m ≠ 0) (z : ℂ) : Function.Periodic.qParam (↑m * h) z ^ m = Function.Periodic.qParam h z

The m-th power of the local parameter at period m * h is the local parameter at period h.

theorem TauCeti.Periodic.sum_qParam_natCast_pow {p : ℕ} (m : ℕ) : ∑ b ∈ Finset.range p, Function.Periodic.qParam ↑p ↑b ^ m = if p ∣ m then ↑p else 0

Orthogonality of the p-th roots of unity, in the local-parameter spelling: the values 𝕢 p b = exp (2 π I b / p) at the integer offsets b < p are the p-th roots of unity, so summing their m-th powers gives p when p ∣ m and 0 otherwise.

This is the identity that makes a sum over the offsets b < p of a translated q-expansion pick out the coefficients in the arithmetic progression p ℕ.

theorem TauCeti.Periodic.hasDerivAt_qParam (h : ℝ) (z : ℂ) : HasDerivAt (Function.Periodic.qParam h) (Function.Periodic.qParam h z * (2 * ↑Real.pi * Complex.I / ↑h)) z

The q-parameter differentiates to itself times 2πi/h. For h = 0 the parameter is the constant 1, whose derivative is genuinely 0 — the value the division junk 2πi/0 = 0 also produces — so the statement is unconditional.

@[simp]

theorem TauCeti.Periodic.deriv_qParam (h : ℝ) (z : ℂ) : deriv (Function.Periodic.qParam h) z = Function.Periodic.qParam h z * (2 * ↑Real.pi * Complex.I / ↑h)

The derivative of the q-parameter, in rewrite form.

theorem TauCeti.Periodic.logDeriv_eq_logDeriv_cuspFunction_mul_deriv_qParam {h : ℝ} {g : ℂ → ℂ} (hh : h ≠ 0) (hg : Function.Periodic g ↑h) (z : ℂ) : logDeriv g z = logDeriv (Function.Periodic.cuspFunction h g) (Function.Periodic.qParam h z) * deriv (Function.Periodic.qParam h) z

The chain rule for the logarithmic derivative of a periodic function through its cusp function: logDeriv g factors through logDeriv (cuspFunction h g) along the q-parameter, for nonzero width h. The statement needs no differentiability: where g is not differentiable, neither is the cusp function at 𝕢 h z — the composition cuspFunction h g ∘ 𝕢 h is g — so both logarithmic derivatives take the junk value 0.