OAI/Analysis/CircleDomains/Probability/PathIntersectionMeasure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The finite intersection measure of a random path with a closed set. Closed incidence tests suffice for measurability of the whole measure. Paths with infinitely many intersections are discarded; they form a null set whenever the expected total intersection count is finite.

  1. theorem OAI.CircleDomainRigidity.pathImageCount_eq_count line 22
  2. def OAI.CircleDomainRigidity.pathIntersectionMeasure line 33
  3. theorem OAI.CircleDomainRigidity.pathIntersectionMeasure_finite line 37
  4. theorem OAI.CircleDomainRigidity.pathIntersectionMeasure_apply line 46
  5. theorem OAI.CircleDomainRigidity.measurable_pathIntersectionMeasure line 60
  6. def OAI.CircleDomainRigidity.meanPathIntersectionMeasure line 75
  7. theorem OAI.CircleDomainRigidity.meanPathIntersectionMeasure_apply line 78
  8. theorem OAI.CircleDomainRigidity.meanPathIntersectionMeasure_finite line 89
  9. theorem OAI.CircleDomainRigidity.meanPathIntersectionMeasure_apply_subset line 97
  10. theorem OAI.CircleDomainRigidity.meanPathIntersectionMeasure_map_null line 105