circleTransformDeriv_periodic — Mathlib

English

The function CircleTransformDeriv is 2π-periodic in its θ-argument.

Русский

Функция CircleTransformDeriv периодична с периодом 2π по аргументу θ.

LaTeX

$$$$ \\text{Periodic}(\\mathrm{circleTransformDeriv}(R,z,w,f),\\ 2\\pi). $$$$

Lean4

theorem circleTransformDeriv_periodic (f : ℂ → E) : Periodic (circleTransformDeriv R z w f) (2 * π) :=
  by
  have := periodic_circleMap
  simp_rw [Periodic] at *
  intro x
  simp_rw [circleTransformDeriv, this]
  congr 2
  simp [this]

Похожие утверждения