LocalizedNuclearHardy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A cutoff Hardy estimate for the near-node part of the nuclear mesh. The right side is localized, allowing bounded-overlap summation over nuclei.