torusIntegral_dim0 — Mathlib

English

In dimension zero, torus integral equals f(c) for f: ℂ^0 → E.

Русский

В размерности 0 тора-интеграл равен f(c).

LaTeX

$$$\operatorname{torusIntegral}(f,c, R) = f(c)$ for n = 0$$

Lean4

@[simp]
theorem torusIntegral_dim0 [CompleteSpace E] (f : (ℂ⁰) → E) (c : ℂ⁰) (R : ℝ⁰) : (∯ x in T(c, R), f x) = f c := by
  simp only [torusIntegral, Fin.prod_univ_zero, one_smul, Subsingleton.elim (fun _ : Fin 0 => 2 * π) 0, Icc_self,
    Measure.restrict_singleton, volume_pi, integral_dirac, Measure.pi_of_empty (fun _ : Fin 0 ↦ volume) 0,
    Measure.dirac_apply_of_mem (mem_singleton _), Subsingleton.elim (torusMap c R 0) c]

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