Theorems · Theorem · several complex variables

torusIntegral_succAbove

∀ {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 →
    ∀ (i : Fin (n + 1)),
      (∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) =
        ∮ (x : ℂ) in C(c i, R i), ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth x y)

Recurrent formula for torusIntegral, see also torusIntegral_succ.

Defined in

Mathlib.MeasureTheory.Integral.TorusIntegral

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace