OAI/InformationTheory/AmplitudeDamping/PhaseCoding.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GAD.signUnitary line 14
2. theorem OAI.GAD.phaseOutput_conjugate line 19
3. theorem OAI.GAD.spectralMatrix_conjugate line 28
4. theorem OAI.GAD.phase_spectral line 35

   Source documentation

   The two phase outputs have a single common eigenvalue distribution.

   theorem phase_spectral (γ ν : ℝ) (hγ : γ ∈ Set.Icc (0:ℝ) 1)
       (hν : ν ∈ Set.Icc (0:ℝ) 1) {p : ℝ} (hp : p ∈ Set.Icc (0:ℝ) 1) :
       ∃ (q : Fin 2 → ℝ) (U : Fin 2 → Matrix.unitaryGroup (Fin 2) ℂ),
         (∀ i, 0 ≤ q i) ∧ (∑ i, q i=1) ∧
         (∀ s, phaseOutput γ ν p s=spectralMatrix (U s) q) ∧
         classicalEntropy q=g (v γ ν p) := by
   …

   Mentions: OAI.GAD.phaseOutput, OAI.GAD.spectralMatrix, OAI.GAD.classicalEntropy, OAI.GAD.g, OAI.GAD.v

5. def OAI.GAD.meanPhaseWeights line 52
6. theorem OAI.GAD.meanPhaseWeights_nonneg line 55
7. theorem OAI.GAD.meanPhaseWeights_sum line 69
8. theorem OAI.GAD.meanPhaseWeights_entropy line 72
9. theorem OAI.GAD.phase_mean_spectral line 77
10. theorem OAI.GAD.exists_phase_code line 92