OAI/Analysis/CircleDomains/Probability/LocalizedSquareMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local square-density estimates for point avoidance. The energy of a shrinking family tends to zero when its intersection is reference-null.

  1. theorem OAI.CircleDomainRigidity.localized_square_mass_bound line 17
  2. theorem OAI.CircleDomainRigidity.tendsto_local_square_energy_zero line 30