OAI/Analysis/CircleDomains/Selection/VisitCounts.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Finite visit witnesses have Borel incidence. The resulting extended count records visits at distinct parameter times, including both endpoints.

  1. def OAI.CircleDomainRigidity.separatedTimeSet line 16
  2. abbrev OAI.CircleDomainRigidity.SeparatedTimes line 19
  3. theorem OAI.CircleDomainRigidity.isClosed_separatedTimeSet line 21
  4. instance OAI.CircleDomainRigidity.(instance at line 26) line 26
  5. def OAI.CircleDomainRigidity.separatedVisitSet line 29
  6. theorem OAI.CircleDomainRigidity.isClosed_separatedVisitSet line 33
  7. def OAI.CircleDomainRigidity.visitAtLeastSet line 55
  8. theorem OAI.CircleDomainRigidity.visitAtLeastSet_eq_iUnion line 59
  9. theorem OAI.CircleDomainRigidity.measurableSet_visitAtLeastSet line 81
  10. def OAI.CircleDomainRigidity.visitCount line 87

    Source documentation

    Extended number of distinct visit times, defined by finite witnesses.

    def visitCount (γ : C(PathTime, X)) (x : X) : ℝ≥0∞ := by
…

    Mentions: OAI.CircleDomainRigidity.PathTime

  11. theorem OAI.CircleDomainRigidity.measurable_visitCount line 91
  12. theorem OAI.CircleDomainRigidity.visitCount_ge_nat line 100
  13. theorem OAI.CircleDomainRigidity.visitCount_eq_zero_of_not_hit line 111
  14. theorem OAI.CircleDomainRigidity.one_le_visitCount_of_hit line 128
  15. def OAI.CircleDomainRigidity.meanVisitCount line 135
  16. theorem OAI.CircleDomainRigidity.pathHitProbability_le_meanVisitCount line 139