Physlib

QuantumInfo.States.Pure.Braket

Finite dimensional quantum pure states, bra and kets. Mixed states are `MState` in that file.

These could be done with a Hilbert space of Fintype, which would look like ```lean4 (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [FiniteDimensional ℂ H] ``` or by choosing a particular `Basis` and asserting it is `Fintype`. But frankly it seems easier to mostly focus on the basis-dependent notion of `Matrix`, which has the added benefit of an obvious "classical" interpretation (as the basis elements, or diagonal elements of a mixed state). In that sense, this quantum theory comes with the a particular classical theory always preferred.

Norm bounds

2 declarations

theorem

⟨ψ2∣ψ1⟩=⟨ψ1∣ψ2⟩‾\langle \psi_2 | \psi_1 \rangle = \overline{\langle \psi_1 | \psi_2 \rangle}

For any two kets ∣ψ1⟩,∣ψ2⟩∈Ket d|\psi_1\rangle, |\psi_2\rangle \in \text{Ket } d defined over a finite index set dd, the inner product (bra-ket product) satisfies the conjugate symmetry property: ⟨ψ2∣ψ1⟩=⟨ψ1∣ψ2⟩‾\langle \psi_2 | \psi_1 \rangle = \overline{\langle \psi_1 | \psi_2 \rangle} where z‾\overline{z} denotes the complex conjugate of z∈Cz \in \mathbb{C}.

theorem

The norm of the inner product of normalized states ∥⟨ψ1∣ψ2⟩∥\|\langle \psi_1 | \psi_2 \rangle\| is at most 1

Given a finite index set dd, for any two normalized quantum states ∣ψ1⟩|\psi_1\rangle and ∣ψ2⟩|\psi_2\rangle in the ket space Ket d≅Cd\text{Ket } d \cong \mathbb{C}^d, the absolute value of their inner product ⟨ψ1∣ψ2⟩\langle \psi_1 | \psi_2 \rangle is at most 1, i.e., ∥⟨ψ1∣ψ2⟩∥≤1\|\langle \psi_1 | \psi_2 \rangle\| \leq 1 This result is a consequence of the Cauchy-Schwarz inequality applied to normalized vectors.