PairKernelEnergy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The two-sided kernel estimate used for local domain meetings. The reference measure and kernel will be the spherical area and the normalized small-ball indicator; no boundedness of the occupation densities is needed.

theorem OAI.CircleDomainRigidity.pair_kernel_energy_bound line 18