OAI/InformationTheory/AmplitudeDamping/OutputEntropy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GAD.pure_output_entropy_bound line 15

   Source documentation

   The population-dependent lower bound for every pure input, including entangled inputs.

   theorem pure_output_entropy_bound (γ ν : ℝ) (hγ : γ ∈ Set.Icc (0:ℝ) 1)
       (hν : ν ∈ Set.Icc (0:ℝ) 1) (n : ℕ) (ψ : Basis n → ℂ)
       (hψ : vecMass ψ = 1) :
       ∑ j, g (v γ ν (population ψ j)) ≤ entropy (channel γ ν n (pure ψ)) := by
   …

   Mentions: OAI.GAD.Basis, OAI.GAD.vecMass, OAI.GAD.g, OAI.GAD.v, OAI.GAD.population, OAI.GAD.entropy, OAI.GAD.channel, OAI.GAD.pure

2. theorem OAI.GAD.mixed_output_entropy_bound line 58
3. def OAI.GAD.coordinatePerm line 100

   Source documentation

   Relabeling the tensor sites.

   def coordinatePerm {n : ℕ} {α : Type u_1} (e : Equiv.Perm (Fin n)) : (Fin n → α) ≃ (Fin n → α) where
   …

4. theorem OAI.GAD.coordinatePerm_apply line 106
5. theorem OAI.GAD.coordinatePerm_symm_apply line 108
6. theorem OAI.GAD.tensorKraus_reindex line 111
7. theorem OAI.GAD.channel_reindex line 119
8. theorem OAI.GAD.matrixPopulation_reindex line 130
9. theorem OAI.GAD.population_channel_pure_zero line 137
10. theorem OAI.GAD.population_channel_zero line 161
11. theorem OAI.GAD.channel_population line 181