OAI/Analysis/CircleDomains/Selection/DyadicTimes.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The fixed dyadic time partitions used to assemble physical-domain length.

  1. def OAI.CircleDomainRigidity.dyadicReal line 14
  2. theorem OAI.CircleDomainRigidity.dyadicReal_nonneg line 16
  3. theorem OAI.CircleDomainRigidity.dyadicReal_le_one line 20
  4. theorem OAI.CircleDomainRigidity.dyadicReal_mono line 24
  5. theorem OAI.CircleDomainRigidity.dyadicReal_even line 28
  6. def OAI.CircleDomainRigidity.dyadicTime line 34
  7. def OAI.CircleDomainRigidity.dyadicLeft line 37
  8. def OAI.CircleDomainRigidity.dyadicRight line 39
  9. theorem OAI.CircleDomainRigidity.dyadicLeft_le_right line 41
  10. def OAI.CircleDomainRigidity.dyadicEven line 44
  11. def OAI.CircleDomainRigidity.dyadicOdd line 47
  12. theorem OAI.CircleDomainRigidity.dyadicLeft_even line 50
  13. theorem OAI.CircleDomainRigidity.dyadicRight_odd line 55
  14. theorem OAI.CircleDomainRigidity.dyadicRight_even line 62
  15. theorem OAI.CircleDomainRigidity.dyadicCell_split line 65
  16. def OAI.CircleDomainRigidity.dyadicChildrenEquiv line 75
  17. theorem OAI.CircleDomainRigidity.dyadicChildrenEquiv_zero line 78
  18. theorem OAI.CircleDomainRigidity.dyadicChildrenEquiv_one line 83
  19. theorem OAI.CircleDomainRigidity.sum_dyadic_children line 88