Theorems · Theorem · several complex variables

torusIntegral_succ

∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : (Fin (n + 1) → ℂ) → E}
  {c : Fin (n + 1) → ℂ} {R : Fin (n + 1) → ℝ},
  TorusIntegrable f c R →
    (∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) =
      ∮ (x : ℂ) in C(c 0, R 0), ∯ (y : Fin n → ℂ) in T(c ∘ Fin.succ, R ∘ Fin.succ), f (Fin.cons x y)

Recurrent formula for torusIntegral, see also torusIntegral_succAbove.

Defined in

Mathlib.MeasureTheory.Integral.TorusIntegral

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace