OAI/Probability/ClassicalON/BlockGeometry.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ClassicalON.ThreeBlock line 10
  2. def OAI.ClassicalON.splitThree line 12
  3. def OAI.ClassicalON.blockHead line 16
  4. def OAI.ClassicalON.blockTail line 17
  5. def OAI.ClassicalON.blockRadius line 18
  6. theorem OAI.ClassicalON.blockRadius_nonneg line 20
  7. theorem OAI.ClassicalON.blockRadius_le_one line 22
  8. theorem OAI.ClassicalON.block_norm_sq line 26
  9. theorem OAI.ClassicalON.block_inner line 30
  10. theorem OAI.ClassicalON.blockHead_first line 35
  11. theorem OAI.ClassicalON.continuous_blockHead line 37
  12. theorem OAI.ClassicalON.continuous_blockTail line 39
  13. theorem OAI.ClassicalON.continuous_blockRadius line 41
  14. def OAI.ClassicalON.blockDirection line 43
  15. theorem OAI.ClassicalON.block_head_direction line 49
  16. def OAI.ClassicalON.blockFiber line 57
  17. theorem OAI.ClassicalON.blockHead_fiber line 65
  18. theorem OAI.ClassicalON.blockTail_fiber line 68
  19. theorem OAI.ClassicalON.blockFiber_inner line 72
  20. theorem OAI.ClassicalON.continuous_blockFiber line 79
  21. def OAI.ClassicalON.blockRotation line 86
  22. def OAI.ClassicalON.blockRotateSpin line 90
  23. theorem OAI.ClassicalON.blockRotateSpin_fiber line 93
  24. theorem OAI.ClassicalON.continuous_blockRotateSpin line 106