English
A function f: ℂ^n → E is integrable on the generalized torus if f ∘ torusMap(c,R) is integrable on Icc([0, …], [0, 2π]).
Русский
Функция f: ℂ^n → E интегрируема на обобщённом торусе тогда, когда f ∘ torusMap(c,R) интегрируема на Icc.
LaTeX
$$$\\mathrm{TorusIntegrable}(f,c,R)\\;\\Leftrightarrow\\; \\mathrm{IntegrableOn}(\\lambda \\theta, f(\\mathrm{torusMap}(c,R)\\theta), \\mathrm{Icc}(0, 2\\pi))$$$
Lean4
/-- A function `f : ℂⁿ → E` is integrable on the generalized torus if the function
`f ∘ torusMap c R θ` is integrable on `Icc (0 : ℝⁿ) (fun _ ↦ 2 * π)`. -/
def TorusIntegrable (f : (ℂⁿ) → E) (c : ℂⁿ) (R : ℝⁿ) : Prop :=
IntegrableOn (fun θ : ℝⁿ => f (torusMap c R θ)) (Icc (0 : ℝⁿ) fun _ => 2 * π) volume
