OAI/InformationTheory/AmplitudeDamping/Model.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.GAD.Basis line 13

   Also declared: ComparatorChallenges/AmplitudeDamping.lean:13 (same declaration text).

2. abbrev OAI.GAD.QMatrix line 14

   Also declared: ComparatorChallenges/AmplitudeDamping.lean:14 (same declaration text).

3. def OAI.GAD.entropy line 17

   Source documentation

   The spectral definition of -Tr(P log P), with 0 log 0 = 0.

   Also declared: ComparatorChallenges/AmplitudeDamping.lean:17 (same declaration text).

   def entropy {ι : Type u} [Fintype ι] [DecidableEq ι] (P : Matrix ι ι ℂ) : ℝ :=
   …

4. def OAI.GAD.IsState line 20

   Also declared: ComparatorChallenges/AmplitudeDamping.lean:20 (same declaration text).

5. def OAI.GAD.kraus line 24

   Also declared: ComparatorChallenges/AmplitudeDamping.lean:24 (same declaration text).

6. def OAI.GAD.tensorKraus line 36

   Source documentation

   Tensor products of the single-site Kraus operators, with the full Kraus index.

   Also declared: ComparatorChallenges/AmplitudeDamping.lean:36 (same declaration text).

   def tensorKraus (γ ν : ℝ) (n : ℕ) (r : Fin n → Fin 4) : QMatrix n :=
   …

   Mentions: OAI.GAD.QMatrix

7. def OAI.GAD.channel line 40

   Source documentation

   The memoryless n-fold generalized amplitude-damping channel.

   Also declared: ComparatorChallenges/AmplitudeDamping.lean:40 (same declaration text).

   def channel (γ ν : ℝ) (n : ℕ) (P : QMatrix n) : QMatrix n :=
   …

   Mentions: OAI.GAD.QMatrix

8. structure OAI.GAD.Ensemble line 45

   Source documentation

   All finite ensembles, without any product or purity restriction.

   Also declared: ComparatorChallenges/AmplitudeDamping.lean:45 (same declaration text).

   structure Ensemble (n : ℕ) where
   …

9. def OAI.GAD.ensembleValue line 53

   Also declared: ComparatorChallenges/AmplitudeDamping.lean:53 (same declaration text).

10. def OAI.GAD.holevo line 58

    Also declared: ComparatorChallenges/AmplitudeDamping.lean:58 (same declaration text).

11. structure OAI.GAD.Code line 62

    Source documentation

    An unrestricted n-use quantum code with one collective output POVM.

    Also declared: ComparatorChallenges/AmplitudeDamping.lean:62 (same declaration text).

    structure Code (n : ℕ) where
    …

12. def OAI.GAD.averageError line 71

    Also declared: ComparatorChallenges/AmplitudeDamping.lean:71 (same declaration text).

13. def OAI.GAD.Achievable line 77

    Source documentation

    The liminf rate condition written as its eventual lower-bound characterization. There is no preshared entanglement, feedback, or restriction on encodings/decoding.

    Also declared: ComparatorChallenges/AmplitudeDamping.lean:77 (same declaration text).

    def Achievable (γ ν R : ℝ) : Prop :=
    …

14. def OAI.GAD.capacity line 84

    Source documentation

    Operational unassisted classical capacity, not a definition by regularization.

    Also declared: ComparatorChallenges/AmplitudeDamping.lean:84 (same declaration text).

    def capacity (γ ν : ℝ) : ℝ := sSup {R : ℝ | Achievable γ ν R}

    Mentions: OAI.GAD.Achievable

15. def OAI.GAD.g line 86

    Also declared: ComparatorChallenges/AmplitudeDamping.lean:86 (same declaration text).

16. def OAI.GAD.v line 88

    Also declared: ComparatorChallenges/AmplitudeDamping.lean:88 (same declaration text).

17. def OAI.GAD.objective line 90

    Also declared: ComparatorChallenges/AmplitudeDamping.lean:90 (same declaration text).

18. def OAI.GAD.Maximizes line 93

    Also declared: ComparatorChallenges/AmplitudeDamping.lean:93 (same declaration text).

19. def OAI.GAD.phaseSignal line 97

    Also declared: ComparatorChallenges/AmplitudeDamping.lean:97 (same declaration text).

20. def OAI.GAD.phaseProduct line 101

    Also declared: ComparatorChallenges/AmplitudeDamping.lean:101 (same declaration text).

21. def OAI.GAD.phaseState line 104

    Also declared: ComparatorChallenges/AmplitudeDamping.lean:104 (same declaration text).

22. def OAI.GAD.phaseValue line 108

    Source documentation

    Holevo value of the explicit 2^n equiprobable product signals.

    Also declared: ComparatorChallenges/AmplitudeDamping.lean:108 (same declaration text).

    def phaseValue (γ ν p : ℝ) (n : ℕ) : ℝ :=
    …