OAI/LinearAlgebra/MatrixFields/Entropy/JointAmbientEntropy.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.empiricalFiniteLaw line 25
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.empiricalFiniteLaw_mass line 32
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.empiricalFiniteLaw_map_mass line 36
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.empiricalFiniteLaw_supported line 44
  5. def OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.canonicalLaw line 59
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.canonicalLaw_mass_of_pos line 64
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.total_mul_canonicalLaw_mass line 71
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.localAllowed_marginal_eq line 86
  9. def OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.gibbsCap line 97
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.gibbsCap_nonneg line 103
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.localAllowed_entropy_le_of_word_support line 109
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.localAllowed_entropy_le line 132
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.sharedAmbient_card_le_of_supported_gibbs line 148
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.neighbors_card_le_of_supported_gibbs line 160
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.sharedAmbient_card_le_of_gibbs line 173
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.neighbors_card_le_of_gibbs line 185
  17. def OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.classScale line 200
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.classScale_nonneg line 203
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.classScale_mul_canonicalLaw_mass line 206
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.classScale_mul_canonicalLaw_map_mass line 214
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.classScale_mul_marginalError line 226
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.tendsto_classScale line 243
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.tendsto_classScale_mul_marginalError line 251
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.JointAmbientEntropy.tendsto_classScale_mul_gibbsCap line 278