English
The torus integral is defined as the integral over θ in Icc(0,2π)^n of the torus-derivative factor times f(torusMap(c,R,θ)).
Русский
Торо-интеграл определяется как интеграл по θ на Icc(0,2π)^n от torus-деривативного множителя, умноженного на f(torusMap(c,R,θ)).
LaTeX
$$$\operatorname{torusIntegral}(f,c,R) = \int_{\theta \in Icc(0,2\pi)^n} \left(\prod_i R_i e^{\theta_i I} I\right) \cdot f(\mathrm{torusMap}(c,R,\theta)) \, d\theta$$$
Lean4
/-- The integral over a generalized torus with center `c ∈ ℂⁿ` and radius `R ∈ ℝⁿ`, defined
as the `•`-product of the derivative of `torusMap` and `f (torusMap c R θ)` -/
def torusIntegral (f : (ℂⁿ) → E) (c : ℂⁿ) (R : ℝⁿ) :=
∫ θ : ℝⁿ in Icc (0 : ℝⁿ) fun _ => 2 * π, (∏ i, R i * exp (θ i * I) * I : ℂ) • f (torusMap c R θ)
