Fubini's theorem for integrals over cycles #
For cycles C and D and a function F z w jointly continuous on the product of their traces,
the two iterated integrals agree:
∫_C (∫_D F z w dw) dz = ∫_D (∫_C F z w dz) dw.
Iterated cycle integrals arise in the holomorphic functional calculus, where the product of two resolvent integrals over nested cycles is a double integral over both cycles.
Main results #
TauCeti.Contour.Cycle.integral_integral_swap: the order of integration over two cycles can be exchanged for integrands continuous on the product of the traces.
theorem
TauCeti.Contour.Cycle.integral_integral_swap
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{F : ℂ → ℂ → E}
{C D : Cycle}
(hF : ContinuousOn (Function.uncurry F) (C.trace ×ˢ D.trace))
:
Fubini's theorem for cycles. For a function F continuous on the product of the traces of
two cycles C and D,
∫_C (∫_D F z w dw) dz = ∫_D (∫_C F z w dz) dw.