Theorems · Theorem · several complex variables

torusIntegral_dim1

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : (Fin 1 → ℂ) → E) (c : Fin 1 → ℂ)
  (R : Fin 1 → ℝ), (∯ (x : Fin 1 → ℂ) in T(c, R), f x) = ∮ (z : ℂ) in C(c 0, R 0), f fun x => z

In dimension one, torusIntegral is the same as circleIntegral (up to the natural equivalence between ℂ and Fin 1 → ℂ).

Defined in

Mathlib.MeasureTheory.Integral.TorusIntegral

Cited by

0 results in Mathlib

Foundations

Depth 258 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace