OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/GroupedEntropyEmbedding.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.groupMass_label_injective line 19
  2. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.groupLaw_label_injective line 25
  3. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.groupMass_label_not_mem_range line 33
  4. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.groupedEntropy_label_injective line 40
  5. def OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.pushforwardWeight line 51
  6. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.sum_pushforwardWeight_mul line 54
  7. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.groupMass_pushforward line 64
  8. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.groupMeasure_pushforward line 71
  9. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.groupLaw_pushforward line 80
  10. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.groupedEntropy_pushforward line 90
  11. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.groupedEntropy_pushforward_of_agree line 96
  12. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.groupedEntropy_pushforward_embedding line 105
  13. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.sum_map_mass_mul line 114
  14. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.groupMass_map line 120
  15. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.groupMeasure_map line 127
  16. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.groupLaw_map line 136
  17. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.groupedEntropy_map line 144
  18. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.groupedEntropy_map_of_agree line 150
  19. theorem OAI.MatrixMultiplication.JointGroupedEntropyEmbedding.groupedEntropy_map_embedding line 159