OAI/Analysis/CircleDomains/Modulus/DyadicTimeLength.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The atomless time arclength measure on the open physical-domain times.

  1. def OAI.CircleDomainRigidity.physicalStageTimeLength line 18
  2. theorem OAI.CircleDomainRigidity.physicalDyadicTimeLength_split line 22
  3. theorem OAI.CircleDomainRigidity.physicalDyadicTimeLength_le_children line 62
  4. theorem OAI.CircleDomainRigidity.monotone_physicalStageTimeLength line 75
  5. def OAI.CircleDomainRigidity.physicalTimeLength line 84
  6. theorem OAI.CircleDomainRigidity.physicalTimeLength_apply line 88
  7. theorem OAI.CircleDomainRigidity.physicalStageTimeLength_univ line 93
  8. theorem OAI.CircleDomainRigidity.physicalTimeLength_univ line 100
  9. instance OAI.CircleDomainRigidity.(instance at line 106) line 106
  10. instance OAI.CircleDomainRigidity.(instance at line 110) line 110
  11. theorem OAI.CircleDomainRigidity.measurable_physicalTimeLength line 120