A residue formula for integrals with hyperplane singularities

6 Residues and integrals

Definition 28 Flag residue
✓
#

Uses

Lean declarations

The flag residue for a selection \(\sigma \): computed by iterating \(\mathrm{poleIn0}\) through the restricted forms at each step.

Definition 29 Convergence hypothesis
✓
#

Lean declarations

The convergence hypothesis: \(\mathrm{Re}(s) {\gt} 0\) and UHP-filtered convergence (the Cauchy residue identity holds at each step of the iterated integral).

Lemma 30 Integrand equals generalized integrand
✓
#

Lean declarations

The original integrand with real linear forms equals the generalized integrand constructed via \(\mathrm{ofRealForm}\).

Proof ▶

Direct computation.

Theorem 31 UHP-filtered expansion
✓
#

Uses

Lean declarations

Under UHP-filtered convergence, the integral equals \((2\pi i)^n\) times the sum over UHP-arising selections only.

Proof ▶

Induction on UHP-filtered convergence.