OAI/Analysis/CircleDomains/Modulus/CountableImageIncidence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Incidence bounds for the countable image exposed by discarded constant tags. The estimate charges parameter times, and hence retains multiplicity.

  1. def OAI.CircleDomainRigidity.timeIncidence line 17
  2. def OAI.CircleDomainRigidity.timeToll line 20
  3. theorem OAI.CircleDomainRigidity.timeToll_eq_indicator line 23
  4. theorem OAI.CircleDomainRigidity.timeIncidence_iUnion line 27
  5. theorem OAI.CircleDomainRigidity.timeToll_mono line 37
  6. theorem OAI.CircleDomainRigidity.timeToll_iUnion line 41
  7. theorem OAI.CircleDomainRigidity.countable_image_incidence_bound line 48
  8. theorem OAI.CircleDomainRigidity.countable_image_deleted_incidence_bound line 74
  9. theorem OAI.CircleDomainRigidity.timeIncidence_bound_of_disjoint_cover line 84