GaussianKernelFubini.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The Gaussian/character integral may be interchanged with an integrable scalar kernel. This is the actual Fubini step of dual regularization.

theorem OAI.WeakPureInfiniteness.gaussian_character_kernel_integral line 14