OAI/Analysis/CircleDomains/Selection/DustPriorContacts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Prior constraints only charge residual times in the dust. Consequently their finite-toll argument only needs visit bounds at dust marks; a possible atom at the image of infinity does not impose an extra path constraint.

  1. def OAI.CircleDomainRigidity.dustPriorHitMass line 15
  2. theorem OAI.CircleDomainRigidity.support_dustPriorHitMass line 19
  3. theorem OAI.CircleDomainRigidity.residualToll_dust_restriction line 25
  4. theorem OAI.CircleDomainRigidity.ae_code_dust_prior_envelope_null line 40
  5. theorem OAI.CircleDomainRigidity.ae_later_residual_contact_in_prior_support_of_dust_bounds line 61