OAI/Probability/ClassicalON/BlockOrbit.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ClassicalON.orthogonalSpin_eval_preserves line 12
  2. def OAI.ClassicalON.blockFiberConfiguration line 25
  3. theorem OAI.ClassicalON.continuous_blockFiberConfiguration line 29
  4. def OAI.ClassicalON.blockRotateConfiguration line 37
  5. theorem OAI.ClassicalON.blockRotateConfiguration_fiber line 42
  6. theorem OAI.ClassicalON.continuous_blockRotateConfiguration line 49
  7. theorem OAI.ClassicalON.blockRotateConfiguration_preserves line 57
  8. def OAI.ClassicalON.orthogonalConfigurationLaw line 62
  9. instance OAI.ClassicalON.orthogonalConfigurationLaw_isProbability line 63
  10. theorem OAI.ClassicalON.integral_block_orbit line 67
  11. theorem OAI.ClassicalON.integral_freeSpinReference_block line 84