OAI/Analysis/CircleDomains/Topology/ResidualClosedIntervals.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Singleton incidence estimates supply the endpoints omitted by open pieces. The original rational constraints therefore hold on every closed time interval, without a local finiteness assumption on the prior toll.

  1. theorem OAI.CircleDomainRigidity.residualToll_union line 19
  2. theorem OAI.CircleDomainRigidity.residualIncidence_time_union line 34
  3. theorem OAI.CircleDomainRigidity.residualIncidenceBound_union line 48
  4. theorem OAI.CircleDomainRigidity.residualToll_singleton line 58
  5. theorem OAI.CircleDomainRigidity.residualIncidenceBound_singleton line 64
  6. theorem OAI.CircleDomainRigidity.residualIncidenceBound_closed_of_open line 86
  7. theorem OAI.CircleDomainRigidity.residualIncidenceBound_closed_of_rational line 106
  8. theorem OAI.CircleDomainRigidity.residualConstraintFamily_closed line 115