OAI/Analysis/CircleDomains/Selection/ResidualVisits.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Actual residual visit multiplicities and tolls on closed test intervals.

  1. def OAI.CircleDomainRigidity.residualVisitRelation line 18
  2. theorem OAI.CircleDomainRigidity.isClosed_residualVisitRelation line 22
  3. def OAI.CircleDomainRigidity.residualVisitCount line 29
  4. def OAI.CircleDomainRigidity.residualToll line 32
  5. theorem OAI.CircleDomainRigidity.residualToll_eq_visits line 35
  6. theorem OAI.CircleDomainRigidity.residualToll_eq_support line 51
  7. theorem OAI.CircleDomainRigidity.measurable_residualVisitCount line 66
  8. theorem OAI.CircleDomainRigidity.measurable_residualToll line 71
  9. theorem OAI.CircleDomainRigidity.measurable_residualToll_of_summable_sq line 80