OAI/Analysis/CircleDomains/Probability/LocalMassVanishing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A quadratic area bound and a linear occupation lower bound force a point-hit probability to vanish. This is the local L² estimate.

  1. theorem OAI.CircleDomainRigidity.local_mass_vanishing line 14