OAI/Analysis/CircleDomains/Modulus/PhysicalDyadicLength.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Borel dyadic physical length and finite-stage occupation data. Every length here uses the physical metric after inverting the quotient.

  1. def OAI.CircleDomainRigidity.physicalDyadicPath line 20
  2. def OAI.CircleDomainRigidity.physicalDyadicLength line 24
  3. def OAI.CircleDomainRigidity.physicalStageLength line 28
  4. def OAI.CircleDomainRigidity.physicalDomainLength line 31
  5. theorem OAI.CircleDomainRigidity.physicalDyadicLength_le_domain line 34
  6. theorem OAI.CircleDomainRigidity.physicalDyadicPath_rectifiable line 40
  7. theorem OAI.CircleDomainRigidity.measurable_physicalDyadicLength line 48
  8. theorem OAI.CircleDomainRigidity.measurable_physicalDomainLength line 53
  9. theorem OAI.CircleDomainRigidity.measurableSet_finitePhysicalDomainLength line 59
  10. def OAI.CircleDomainRigidity.physicalStageOccupation line 65
  11. theorem OAI.CircleDomainRigidity.physicalStageOccupation_univ line 70
  12. theorem OAI.CircleDomainRigidity.measurable_physicalStageOccupation line 77