OAI/NumberTheory/PrimePackets/ShannonEntropy.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.finiteShannon line 42
  2. lemma OAI.PrimeDegreePackets.finiteShannon_nonneg line 45
  3. lemma OAI.PrimeDegreePackets.negMulLog_le_cross line 54
  4. theorem OAI.PrimeDegreePackets.finiteShannon_le_cross line 72
  5. theorem OAI.PrimeDegreePackets.finiteShannon_joint_le line 85
  6. theorem OAI.PrimeDegreePackets.finiteShannon_le_log_card line 125
  7. def OAI.PrimeDegreePackets.observationEntropy line 142
  8. lemma OAI.PrimeDegreePackets.observation_distribution_sum line 146
  9. lemma OAI.PrimeDegreePackets.observationEntropy_nonneg line 159
  10. lemma OAI.PrimeDegreePackets.observationEntropy_equiv line 170
  11. lemma OAI.PrimeDegreePackets.observation_joint_row line 178
  12. theorem OAI.PrimeDegreePackets.observationEntropy_joint_le line 197
  13. lemma OAI.PrimeDegreePackets.observationEntropy_comp_preserving line 219
  14. def OAI.PrimeDegreePackets.orbitName line 231
  15. lemma OAI.PrimeDegreePackets.orbitName_measurable_fiber line 234
  16. lemma OAI.PrimeDegreePackets.orbitName_add line 244
  17. theorem OAI.PrimeDegreePackets.orbitEntropy_subadditive line 257
  18. def OAI.PrimeDegreePackets.observationEntropyRate line 276
  19. theorem OAI.PrimeDegreePackets.tendsto_observationEntropyRate line 281
  20. def OAI.PrimeDegreePackets.measureEntropy line 296
  21. lemma OAI.PrimeDegreePackets.negMulLog_lower_of_le_exp line 306
  22. theorem OAI.PrimeDegreePackets.finiteShannon_split_lower line 319
  23. lemma OAI.PrimeDegreePackets.sum_good_observation_masses line 356
  24. theorem OAI.PrimeDegreePackets.observationEntropy_lower_of_good_atoms line 372
  25. theorem OAI.PrimeDegreePackets.observationEntropyRate_lower_of_good_atoms line 391
  26. theorem OAI.PrimeDegreePackets.measureEntropy_lower_of_good_atoms line 435