English
If ‖f(torusMap(c,R,θ))‖ ≤ C for all θ, then the norm of the torus integral is bounded by ((2π)^n ∏ |R_i|) C.
Русский
Если для всех θ выполнено ≤ C, тогда ‖torusIntegral(f,c,R)‖ ≤ ((2π)^n ∏ |R_i|) C.
LaTeX
$$If ∀θ, ‖f(torusMap(c,R,θ))‖ ≤ C, then ∥torusIntegral(f,c,R)∥ ≤ ((2π)^n ∏ i |R_i|) C$$
Lean4
/-- If for all `θ : ℝⁿ`, `‖f (torusMap c R θ)‖` is less than or equal to a constant `C : ℝ`, then
`‖∯ x in T(c, R), f x‖` is less than or equal to `(2 * π)^n * (∏ i, |R i|) * C` -/
theorem norm_torusIntegral_le_of_norm_le_const {C : ℝ} (hf : ∀ θ, ‖f (torusMap c R θ)‖ ≤ C) :
‖∯ x in T(c, R), f x‖ ≤ ((2 * π) ^ (n : ℕ) * ∏ i, |R i|) * C :=
calc
‖∯ x in T(c, R), f x‖ ≤ (∏ i, |R i|) * C * (volume (Icc (0 : ℝⁿ) fun _ => 2 * π)).toReal :=
norm_setIntegral_le_of_norm_le_const measure_Icc_lt_top fun θ _ =>
calc
‖(∏ i : Fin n, R i * exp (θ i * I) * I : ℂ) • f (torusMap c R θ)‖ =
(∏ i : Fin n, |R i|) * ‖f (torusMap c R θ)‖ :=
by simp [norm_smul]
_ ≤ (∏ i : Fin n, |R i|) * C := mul_le_mul_of_nonneg_left (hf _) <| by positivity
_ = ((2 * π) ^ (n : ℕ) * ∏ i, |R i|) * C := by
simp only [Pi.zero_def, Real.volume_Icc_pi_toReal fun _ => Real.two_pi_pos.le, sub_zero, Fin.prod_const,
mul_assoc, mul_comm ((2 * π) ^ (n : ℕ))]
