torusMap — Mathlib

English

Define the map θ ↦ c + R e^{θ I} componentwise on ℂ^n.

Русский

Определим отображение торуса по координатам: θ_i ↦ c_i + R_i e^{θ_i i}.

LaTeX

$$$\\mathrm{torusMap}(c,R)(\\theta)(i) = c(i) + R(i) \\cdot e^{\\theta(i) i}$$$

Lean4

/-- The n-dimensional exponential map $θ_i ↦ c + R e^{θ_i*I}, θ ∈ ℝⁿ$ representing
a torus in `ℂⁿ` with center `c ∈ ℂⁿ` and generalized radius `R ∈ ℝⁿ`, so we can adjust
it to every n axis. -/
def torusMap (c : ℂⁿ) (R : ℝⁿ) : (ℝⁿ) → ℂⁿ := fun θ i => c i + R i * exp (θ i * I)

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