OAI/Analysis/CircleDomains/Probability/CodeHitMeasures.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Fubini for complete path images. At free points, tuple absolute continuity reduces a path hit to a residual hit; residual nullity then annihilates the integrated whole-image hit probability.

  1. def OAI.CircleDomainRigidity.codeHitGraph line 19
  2. def OAI.CircleDomainRigidity.codeResidualGraph line 22
  3. theorem OAI.CircleDomainRigidity.isClosed_codeHitGraph line 25
  4. theorem OAI.CircleDomainRigidity.isClosed_codeResidualGraph line 29
  5. def OAI.CircleDomainRigidity.codeHitProbability line 34
  6. def OAI.CircleDomainRigidity.codeResidualProbability line 38
  7. theorem OAI.CircleDomainRigidity.measurable_codeHitProbability line 44
  8. theorem OAI.CircleDomainRigidity.measurable_codeResidualProbability line 48
  9. theorem OAI.CircleDomainRigidity.lintegral_codeResidualProbability line 52
  10. theorem OAI.CircleDomainRigidity.codeHitProbability_eq_residual line 60
  11. theorem OAI.CircleDomainRigidity.lintegral_codeHitProbability_zero line 70