OAI/Analysis/CircleDomains/Selection/AtomicHitTests.lean

GitHub source file

6 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. def OAI.CircleDomainRigidity.positiveAtoms line 22
  2. theorem OAI.CircleDomainRigidity.countable_positiveAtoms line 25
  3. theorem OAI.CircleDomainRigidity.nullSingleton_restrict_compl_positiveAtoms line 30
  4. def OAI.CircleDomainRigidity.HasAtomicSquareBound line 40
  5. theorem OAI.CircleDomainRigidity.PassesHitTests.lintegral_le_of_atomic_square_bound line 44
  6. theorem OAI.CircleDomainRigidity.exists_test_law_for_atomic_measure line 88