OAI/InformationTheory/AmplitudeDamping/PhaseStates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GAD.entropy_qubit line 13

   Source documentation

   Entropy of any Hermitian trace-one two-level matrix, expressed through its determinant.

   theorem entropy_qubit {P : Matrix (Fin 2) (Fin 2) ℂ} (hP : P.IsHermitian)
       (htr : P.trace=1) : entropy P = g P.det.re := by
   …

   Mentions: OAI.GAD.entropy, OAI.GAD.g

2. def OAI.GAD.phaseOutput line 48
3. theorem OAI.GAD.phaseSignal_mass line 51
4. theorem OAI.GAD.phaseOutput_state line 57
5. theorem OAI.GAD.phaseOutput_formula line 63
6. theorem OAI.GAD.phaseOutput_det line 78
7. theorem OAI.GAD.phaseOutput_entropy line 90
8. theorem OAI.GAD.phaseOutput_average line 96
9. theorem OAI.GAD.phaseOutput_average_entropy line 104