OAI/Analysis/CircleDomains/Selection/MarkedConfigurations.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Separated configurations lie in the dust test space, while their hit probabilities come from paths in the ambient space.

  1. def OAI.CircleDomainRigidity.MarkedHit.weightedConfigurationHits line 18
  2. theorem OAI.CircleDomainRigidity.MarkedHit.weightedConfigurationHits_nonneg line 22
  3. theorem OAI.CircleDomainRigidity.MarkedHit.weightedConfigurationHits_le_card line 27
  4. theorem OAI.CircleDomainRigidity.MarkedHit.weightedConfigurationHits_upperSemicontinuous line 41