OAI/Analysis/CircleDomains/Selection/ResidualPieceAssembly.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Assembly of residual-contact estimates on disjoint time pieces. No disjointness of their images is required: a repeated visit is paid again.

  1. theorem OAI.CircleDomainRigidity.timeIncidence_union line 17
  2. theorem OAI.CircleDomainRigidity.timeToll_union line 28
  3. theorem OAI.CircleDomainRigidity.timeIncidence_bound_with_countable_remainder line 41
  4. theorem OAI.CircleDomainRigidity.residualIncidence_eq_timeIncidence line 61
  5. theorem OAI.CircleDomainRigidity.residualToll_eq_timeToll line 73
  6. theorem OAI.CircleDomainRigidity.residualIncidenceBound_of_countable_image line 82
  7. theorem OAI.CircleDomainRigidity.residualIncidenceBound_of_disjoint_pieces line 91