OAI/Analysis/CircleDomains/Selection/AffinePhysicalRestriction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

An affine restriction has at most the original physical-domain length. The estimate uses the actual inverse quotient and its arclength measure.

  1. theorem OAI.CircleDomainRigidity.affinePathTime_clip line 18
  2. theorem OAI.CircleDomainRigidity.pathsInsideOn_affine_image line 28
  3. theorem OAI.CircleDomainRigidity.physicalSubpath_affine line 39
  4. theorem OAI.CircleDomainRigidity.physicalSubpath_affine_length_le line 55
  5. theorem OAI.CircleDomainRigidity.physicalDyadicLength_affine_le line 69
  6. theorem OAI.CircleDomainRigidity.physicalDomainLength_affine_le line 85
  7. theorem OAI.CircleDomainRigidity.physicalDomainLength_affine_finite line 99