### Abstract

This is a formal proof of the uncertainty principle known from quantum mechanics. It is based upon work on complex vector spaces contained in the QHLProver session. The formalization follows the proof outlined in the book "Quantum computation and quantum information" by Nielsen and Chuang.

### License

BSD License

### Topics

- Mathematics/Physics/Quantum information

### Related publications

- Nielsen, M. A., & Chuang, I. L. (2012). Quantum Computation and Quantum Information. https://doi.org/10.1017/cbo9780511976667

### Session Uncertainty_Principle

- Uncertainty_Principle

### Depends on

- Quantum Hoare Logic

### Auto-related entries

- Simultaneous diagonalization of pairwise commuting Hermitian matrices

## Cite

×

Uncertainty_Principle-AFP

    @article{Uncertainty_Principle-AFP,
      author  = {Alexander Treml},
      title   = {Uncertainty Principle},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2024},
      note    = {\url{https://isa-afp.org/entries/Uncertainty_Principle.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest