OAI/Analysis/CircleDomains/Selection/PreterminalVisits.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Visit multiplicities with the terminal parameter omitted. The extended subtraction formula is justified by an exact all-time sum decomposition.

  1. def OAI.CircleDomainRigidity.terminalVisitCount line 18
  2. def OAI.CircleDomainRigidity.preterminalVisitCount line 21
  3. theorem OAI.CircleDomainRigidity.preterminalVisitCount_eq_tsum line 24
  4. theorem OAI.CircleDomainRigidity.visitCount_eq_preterminal_add_terminal line 37
  5. theorem OAI.CircleDomainRigidity.preterminalVisitCount_target line 46
  6. theorem OAI.CircleDomainRigidity.measurable_terminalVisitCount line 59
  7. theorem OAI.CircleDomainRigidity.measurable_preterminalVisitCount line 66