OAI/LinearAlgebra/MatrixFields/Entropy/GroupProjectedEntropy.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.JointNativeGroupedEntropy.groupMeasure line 25
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.JointNativeGroupedEntropy.groupMeasure_total line 30
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.JointNativeGroupedEntropy.groupMeasure_zero_of_mass_zero line 43
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.JointNativeGroupedEntropy.group_term_eq_homogeneous line 65
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.JointNativeGroupedEntropy.groupedEntropy_eq_sum_homogeneous line 79
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.JointNativeGroupedEntropy.homogeneousEntropy_mul_normalized line 87
  7. def OAI.MatrixAllFields.MatrixMultiplication.JointNativeGroupedEntropy.singletonResidualGroup line 99
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.JointNativeGroupedEntropy.singletonResidualGroup_eq_inl line 103
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.JointNativeGroupedEntropy.singletonResidualGroup_eq_inr line 116
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.JointNativeGroupedEntropy.groupMeasure_singleton line 122
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.JointNativeGroupedEntropy.groupMeasure_residual line 131
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.JointNativeGroupedEntropy.groupedEntropy_singletons_residuals line 138
  13. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointNativeGroupedEntropy.SupportIndex line 164
  14. def OAI.MatrixAllFields.MatrixMultiplication.JointNativeGroupedEntropy.ownWeight line 166
  15. def OAI.MatrixAllFields.MatrixMultiplication.JointNativeGroupedEntropy.nativeGroup line 171
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.JointNativeGroupedEntropy.groupedEntropy_eq_native line 178
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyPartition.groupMass_mul line 231
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyPartition.groupMeasure_mul line 241
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyPartition.groupLaw_mul_of_ne_zero line 253
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyPartition.groupedEntropy_mul line 264
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyPartition.groupMeasure_designated_some line 275
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyPartition.groupMeasure_designated_none line 284
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyPartition.groupedEntropy_designated line 291
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyPartition.groupedEntropy_partition line 308
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyPartition.groupedEntropy_conditional_partition line 332
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyPartition.native_groupedEntropy_eq_sum_masked line 353
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyPartition.native_groupedEntropy_eq_sum_conditional line 380
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.groupMass_label_injective line 430
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.groupLaw_label_injective line 436
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.groupMass_label_not_mem_range line 444
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.groupedEntropy_label_injective line 451
  32. def OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.pushforwardWeight line 462
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.sum_pushforwardWeight_mul line 465
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.groupMass_pushforward line 475
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.groupMeasure_pushforward line 482
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.groupLaw_pushforward line 491
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.groupedEntropy_pushforward line 501
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.groupedEntropy_pushforward_of_agree line 507
  39. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.groupedEntropy_pushforward_embedding line 516
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.sum_map_mass_mul line 525
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.groupMass_map line 531
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.groupMeasure_map line 538
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.groupLaw_map line 547
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.groupedEntropy_map line 555
  45. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.groupedEntropy_map_of_agree line 561
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.JointGroupedEntropyEmbedding.groupedEntropy_map_embedding line 570
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.JointProjectedGroupEntropy.groupMass_designated_some line 606
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.JointProjectedGroupEntropy.weighted_groupLaw_designated_some line 611
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.JointProjectedGroupEntropy.groupedEntropy_counts_eq_total_mul line 627
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.JointProjectedGroupEntropy.baseGroupSize_eq_groupMass line 658
  51. theorem OAI.MatrixAllFields.MatrixMultiplication.JointProjectedGroupEntropy.residualCenter_eq_groupLaw line 680
  52. theorem OAI.MatrixAllFields.MatrixMultiplication.JointProjectedGroupEntropy.projectedReferenceEntropy_eq_sum_counts_groupedEntropy line 696
  53. theorem OAI.MatrixAllFields.MatrixMultiplication.JointProjectedGroupEntropy.projectedReferenceEntropy_eq_sum_weighted_groupedEntropy line 718
  54. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeGroupedRates.singletonResidualGroup_transport line 757
  55. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeGroupedRates.singletonResidual_groupedEntropy_reindex line 766
  56. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeGroupedRates.right_conditional_sum_eq line 781
  57. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeGroupedRates.supportSubtypeEquiv line 795
  58. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeGroupedRates.supportIndexEquiv line 803
  59. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeGroupedRates.supportIndexEquiv_get line 808
  60. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeGroupedRates.boundedComplement line 815
  61. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeGroupedRates.boundedComplement_involutive line 821
  62. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeGroupedRates.boundedComplementEquiv line 828
  63. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeGroupedRates.native_right_conditional_sum_eq line 838
  64. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeGroupedRates.native_two_conditional_sums_eq line 900
  65. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeGroupedRates.twoHalfConditionalCost line 930
  66. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeGroupedRates.stageA_twoHalfConditionalCost_eq line 944
  67. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeGroupedRates.stageB_twoHalfConditionalCost_eq line 968
  68. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeGroupedRates.stageA_twoHalfConditionalCost_eq_entropy_sub_capacity line 991
  69. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeGroupedRates.stageB_twoHalfConditionalCost_eq_entropy_sub_capacity line 1001
  70. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupProjectedEntropy.groupedEntropy_congr_law_on_support line 1042
  71. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupProjectedEntropy.groupedEntropy_designated_pushforward line 1056
  72. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupProjectedEntropy.groupedEntropy_const_one line 1071
  73. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupProjectedEntropy.pushforwardWeight_mask line 1086
  74. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupProjectedEntropy.maskedBranchMass line 1107
  75. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupProjectedEntropy.classCounts_cast_eq_pushforward line 1112
  76. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupProjectedEntropy.branchHalfLaw line 1160
  77. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupProjectedEntropy.class_groupedEntropy_eq_masked line 1164
  78. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupProjectedEntropy.maskedBranchMass_eq_conditional line 1184
  79. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupProjectedEntropy.branchConditionalCost line 1195
  80. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupProjectedEntropy.history_projected_entropy_eq line 1205
  81. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupProjectedEntropy.branchConditionalCost_eq line 1219
  82. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupProjectedEntropy.branchConditionalCost_eq_observed line 1283
  83. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupProjectedEntropy.projected_native_entropy_eq line 1303