OAI/Analysis/CircleDomains/Probability/CodePathLaws.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Forgetting the optional tags produces the actual path law. Its full mean visit function differs from the preterminal function by exactly one unit at the prescribed terminal point.

  1. def OAI.CircleDomainRigidity.codePath line 20
  2. theorem OAI.CircleDomainRigidity.measurable_codePath line 22
  3. def OAI.CircleDomainRigidity.codePathLaw line 25
  4. theorem OAI.CircleDomainRigidity.pathHitProbability_codePathLaw line 31
  5. theorem OAI.CircleDomainRigidity.meanVisitCount_codePathLaw line 36
  6. theorem OAI.CircleDomainRigidity.codeHitProbability_le_meanCodeVisits line 58