torusIntegral_succ — Mathlib

English

A recurrence formula for torusIntegral with successor operation.

Русский

Рекуррентная формула для torusIntegral с операцией successor.

LaTeX

$$$\operatorname{torusIntegral}(f,c,R) = \operatorname{circleIntegral}(\cdot, c_0, R_0)$$$$

Lean4

/-- Recurrent formula for `torusIntegral`, see also `torusIntegral_succAbove`. -/
theorem torusIntegral_succ {f : (ℂⁿ ⁺ ¹) → E} {c : ℂⁿ ⁺ ¹} {R : ℝⁿ ⁺ ¹} (hf : TorusIntegrable f c R) :
    (∯ x in T(c, R), f x) = ∮ x in C(c 0, R 0), ∯ y in T(c ∘ Fin.succ, R ∘ Fin.succ), f (Fin.cons x y) := by
  simpa using torusIntegral_succAbove hf 0

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