OAI/InformationTheory/AmplitudeDamping/EnsembleBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GAD.concaveOn_binEntropy line 12

   Source documentation

   Binary Shannon entropy is concave, including the endpoints.

   theorem concaveOn_binEntropy : ConcaveOn ℝ (Set.Icc (0:ℝ) 1) Real.binEntropy := by
   …

2. theorem OAI.GAD.weighted_conditional_eq line 21
3. theorem OAI.GAD.conditional_mem line 28
4. theorem OAI.GAD.negMulLog_split line 35
5. def OAI.GAD.distPopulation line 47
6. theorem OAI.GAD.classical_entropy_le_sum_binary line 50
7. theorem OAI.GAD.entropy_le_sum_populations line 99
8. theorem OAI.GAD.output_entropy_upper line 106
9. theorem OAI.GAD.ensemble_nats_upper line 112
10. theorem OAI.GAD.ensembleValue_upper line 147