OAI/InformationTheory/AmplitudeDamping/Main.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GAD.capacity_formula line 10
2. theorem OAI.GAD.capacity_holevo line 31
3. theorem OAI.GAD.main line 38

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Real, Membership.mem, Set, Set.Icc, OfNat.ofNat, And, Nat, LE.le, Eq, OAI.GAD.holevo, HMul.hMul, Exists, OAI.GAD.Maximizes, HDiv.hDiv, Real.log, OAI.GAD.objective, OAI.GAD.capacity, OAI.GAD.Basis, OAI.GAD.IsState, Fin and 2 more

   Proof uses: And.intro, OAI.GAD.holevo_additive, OAI.GAD.holevo_maximizer, OAI.GAD.capacity_holevo, OAI.GAD.phase_attainment

   44 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: ComparatorChallenges/AmplitudeDamping.lean:113 (same statement text; different proof or body). Qualify references as OAI.GAD.main@path.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.