OAI/Analysis/CircleDomains/Selection/MarkedAtomicHitTests.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Countable and atomless tests control integration against any finite measure whose point masses have square norm at most one. This supplies the test-measure step in finite law splitting; the atomless remainder is the restriction away from the actual positive point masses.

  1. theorem OAI.CircleDomainRigidity.MarkedHit.PassesHitTests.lintegral_le_of_atomic_square_bound line 27
  2. theorem OAI.CircleDomainRigidity.MarkedHit.exists_test_law_for_atomic_measure line 71