English
If f is torus integrable, then the integrand used in the torus integral is integrable on the standard box.
Русский
Если f торусно интегрируема, вектор-интегрант для тора является интегрируемым на стандартном прямоугольнике.
LaTeX
$$$\text{If } \operatorname{TorusIntegrable}(f,c,R)\text{, then } \int_{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 \text{ exists (is integrable).}$$$
Lean4
/-- The function given in the definition of `torusIntegral` is integrable. -/
theorem function_integrable [NormedSpace ℂ E] (hf : TorusIntegrable f c R) :
IntegrableOn (fun θ : ℝⁿ => (∏ i, R i * exp (θ i * I) * I : ℂ) • f (torusMap c R θ)) (Icc (0 : ℝⁿ) fun _ => 2 * π)
volume :=
by
refine (hf.norm.const_mul (∏ i, |R i|)).mono' ?_ ?_
· refine (Continuous.aestronglyMeasurable ?_).smul hf.1; fun_prop
simp [norm_smul]
