OAI/Dynamics/StandardMap/Coupling/FiniteVectorEntropy.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicCoding.cond_vector_subadd line 13
  2. lemma OAI.HyperbolicCoding.shannon_productVector line 51
  3. lemma OAI.HyperbolicCoding.mass_factor_sum line 81
  4. lemma OAI.HyperbolicCoding.cond_eq_channel_average line 88
  5. lemma OAI.HyperbolicCoding.product_channel_coordinate line 105
  6. theorem OAI.HyperbolicCoding.product_channel_entropy_lower line 140
  7. lemma OAI.HyperbolicCoding.mass_finiteWeightLaw_id line 184
  8. def OAI.HyperbolicCoding.finiteChannelLaw line 188
  9. lemma OAI.HyperbolicCoding.finiteChannelLaw_probability line 192
  10. lemma OAI.HyperbolicCoding.finiteChannelLaw_pair_mass line 205
  11. lemma OAI.HyperbolicCoding.finiteChannelLaw_input_mass line 213
  12. theorem OAI.HyperbolicCoding.finiteChannelLaw_entropy line 225
  13. lemma OAI.HyperbolicCoding.channel_joint_l1 line 253
  14. lemma OAI.HyperbolicCoding.channel_joint_lawClose line 265
  15. lemma OAI.HyperbolicCoding.channel_output_lawClose line 294
  16. lemma OAI.HyperbolicCoding.channel_cost_stability line 308
  17. def OAI.HyperbolicCoding.recodingKernel line 352
  18. lemma OAI.HyperbolicCoding.recodingKernel_nonneg line 357
  19. lemma OAI.HyperbolicCoding.recodingKernel_sum line 363
  20. lemma OAI.HyperbolicCoding.recodingKernel_joint line 369
  21. def OAI.HyperbolicCoding.recodingLaw line 376
  22. lemma OAI.HyperbolicCoding.recodingLaw_probability line 381
  23. lemma OAI.HyperbolicCoding.recodingLaw_input_mass line 391
  24. lemma OAI.HyperbolicCoding.recodingLaw_input_coordinate line 399
  25. lemma OAI.HyperbolicCoding.recodingLaw_joint_coordinate line 412
  26. lemma OAI.HyperbolicCoding.recodingLaw_input_law line 427
  27. lemma OAI.HyperbolicCoding.recodingLaw_output_lawClose line 442