periodic_circleMap — Mathlib

English

The circle map is 2π-periodic in θ: circleMap c R (θ + 2π) = circleMap c R θ for all θ.

Русский

Круговая карта имеет период 2π по θ: circleMap c R (θ + 2π) = circleMap c R θ для всех θ.

LaTeX

$$$ \forall \theta,\; circleMap c R (\theta + 2 \pi) = circleMap c R \theta $$$

Lean4

/-- `circleMap` is `2π`-periodic. -/
theorem periodic_circleMap (c : ℂ) (R : ℝ) : Periodic (circleMap c R) (2 * π) := fun θ => by
  simp [circleMap, add_mul, exp_periodic _]

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