OAI/Analysis/CircleDomains/Probability/MarkedHitLaws.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Path hits tested on a compact subset of the ambient path space. The continuous map is the inclusion of the dust in the application; no path is required to lie in that subset.

  1. def OAI.CircleDomainRigidity.MarkedHit.pathHitProbability line 19
  2. def OAI.CircleDomainRigidity.MarkedHit.pathHitReal line 22
  3. theorem OAI.CircleDomainRigidity.MarkedHit.pathHitProbability_le_one line 25
  4. theorem OAI.CircleDomainRigidity.MarkedHit.pathHitReal_nonneg line 29
  5. theorem OAI.CircleDomainRigidity.MarkedHit.pathHitReal_le_one line 32
  6. theorem OAI.CircleDomainRigidity.MarkedHit.measurable_pathHitProbability_point line 39
  7. theorem OAI.CircleDomainRigidity.MarkedHit.pathHitReal_upperSemicontinuous line 44
  8. theorem OAI.CircleDomainRigidity.MarkedHit.integrable_pathHitReal line 52
  9. theorem OAI.CircleDomainRigidity.MarkedHit.pathHitReal_mixture line 60