OAI/LinearAlgebra/MatrixFields/Entropy/GroupBranchLaws.lean

GitHub source file

124 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.tendsto_log_multinomial_div_of_total_div_zero line 20
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.tendsto_log_multinomial_div_of_mass line 56
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.tendsto_total_div_of_coordinate_rates line 79
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.tendsto_empirical_of_coordinate_rates line 88
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.finiteEntropy_scalar line 102
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.weighted_empirical_entropy_eq line 108
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.tendsto_weighted_empirical_entropy_of_coordinate_rates line 135
  8. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.sideCounts line 148
  9. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.sideMass line 151
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.sideCounts_total line 154
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.sideMass_total line 160
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.tendsto_sideCounts_div_of_coordinate_rates line 166
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.target_side_population line 191
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.tendsto_weighted_target_side_entropy line 203
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.tendsto_log_target_card_div line 220
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.tendsto_log_target_card_div_of_coordinate_rates line 236
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulationRates.tendsto_log_targetSet_card_div_of_coordinate_rates line 251
  18. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.branchProbability line 274
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.branchProbability_nonneg line 280
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.branchProbability_total line 287
  21. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.branchLaw line 302
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.branchLaw_mass line 307
  23. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.placedLaw line 310
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.placedLaw_mass line 313
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.placedLaw_mass_branch line 320
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.placedLaw_entropy line 324
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.placedLaw_sideMass line 328
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.branchPopulation_cast_rat line 345
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.branchPopulation_cast line 355
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.jointCounts_cast line 363
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.jointCounts_ratio line 375
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.jointCounts_normalized line 384
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.population_cast_real line 391
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.jointCounts_source_cast line 397
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.jointCounts_source_ratio line 404
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.jointCounts_source_rate line 415
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.populationLength_dilation line 424
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.jointCounts_dilation_ratio line 429
  39. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.jointCounts_dilation_rate line 438
  40. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.orderLaw line 448
  41. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.orderMass line 451
  42. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.orderCounts line 455
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.orderMass_nonneg line 459
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.orderCounts_source_cast line 464
  45. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.orderCounts_source_rate line 472
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveLaws.orderCounts_dilation_rate line 479
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupTargetRate.source_unit_pos line 502
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupTargetRate.source_length_dilation line 506
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupTargetRate.orderCounts_dilation line 511
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupTargetRate.orderCounts_dilation_fun line 519
  51. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupTargetRate.orderCounts_sum line 525
  52. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupTargetRate.baseSize_eq_population line 531
  53. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupTargetRate.baseSize_dilation line 537
  54. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupTargetRate.baseSize_cast_real line 545
  55. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupTargetRate.baseSize_pos line 552
  56. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupTargetRate.base_empirical_eq line 558
  57. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupTargetRate.groupEntropyRate line 566
  58. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupTargetRate.groupEntropyRate_nonneg line 571
  59. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupTargetRate.baseEntropy_eq_groupEntropyRate line 579
  60. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupTargetRate.target_card_pos line 587
  61. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupTargetRate.tendsto_log_target_card_div line 592
  62. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupTargetRate.tendsto_log_targetSet_card_div line 608
  63. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPairConditionalEntropy.entropy_sub_eq_conditional_sum line 630
  64. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldPairConditionalEntropy.stageASplitWeight line 641
  65. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldPairConditionalEntropy.stageBSplitWeight line 647
  66. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPairConditionalEntropy.stageASplitLaw_ownWeight_marginal line 653
  67. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPairConditionalEntropy.stageBSplitLaw_ownWeight_marginal line 658
  68. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPairConditionalEntropy.stageA_entropy_sub_pair_eq_conditional_sum line 663
  69. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldPairConditionalEntropy.stageB_entropy_sub_pair_eq_conditional_sum line 676
  70. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.statisticComplement line 704
  71. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.childLaw_complementary_sides line 710
  72. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.halfLawAt line 724
  73. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.childWeight line 728
  74. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.halfLawAt_eq line 733
  75. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.halfLawAt_nonnegative line 741
  76. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.halfLawAt_normalized line 748
  77. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.halfLawAt_le_one_of_counts_pos line 756
  78. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.supportedHalfLaw line 766
  79. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.supportedHalfLaw_bounds line 770
  80. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.supportedHalfLaw_eq_of_counts_pos line 780
  81. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.placedLaw_mass_zero_of_count_zero line 789
  82. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.halfShape_childWeight line 799
  83. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.halfShape_mem_of_counts_pos line 807
  84. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.childWeight_sum line 816
  85. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.designated_source_geometry line 830
  86. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.compatibilityLaw_eq line 847
  87. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.nativePairLaw line 891
  88. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.placedLaw_sum_mul line 903
  89. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.childLaw_branchShape line 910
  90. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.rightChildLaw_branchShape line 918
  91. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.branchPairMixture_eq_native line 928
  92. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.placedPairMixture line 958
  93. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.placedPairMixture_eq_native line 962
  94. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.placement_symm_order_side line 970
  95. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.orderPairMixture line 977
  96. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.orderPairMixture_eq_native line 983
  97. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.orderPairMixture_supported line 991
  98. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.orderPairMixture_nonneg line 1008
  99. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.orderPairMixture_total line 1014
  100. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.orderPairMixture_entropy line 1020
  101. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.nativeStatisticWeightCode line 1029
  102. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.nativeSplitWeightCode line 1035
  103. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.nativeSplitWeightCode_val line 1039
  104. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.nativePairLaw_weight_marginal line 1042
  105. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.commonWeight_law_ext line 1061
  106. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.order_branch_weight line 1071
  107. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.orderLaw_weight_marginal line 1079
  108. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.orderPairLaw_common_weight line 1098
  109. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.order_entropy_sub_pair_eq_conditional_sum line 1105
  110. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupNativeLaws.order_entropy_sub_mixture_eq_conditional_sum line 1117
  111. def OAI.MatrixAllFields.MatrixMultiplication.JointConditionalCountEntropy.classCounts line 1145
  112. def OAI.MatrixAllFields.MatrixMultiplication.JointConditionalCountEntropy.classSize line 1148
  113. theorem OAI.MatrixAllFields.MatrixMultiplication.JointConditionalCountEntropy.classSize_total line 1151
  114. theorem OAI.MatrixAllFields.MatrixMultiplication.JointConditionalCountEntropy.sum_masked_entropy line 1158
  115. theorem OAI.MatrixAllFields.MatrixMultiplication.JointConditionalCountEntropy.sum_classCounts_entropy line 1170
  116. theorem OAI.MatrixAllFields.MatrixMultiplication.JointConditionalCountEntropy.sum_scaled_class_empirical_entropy line 1182
  117. theorem OAI.MatrixAllFields.MatrixMultiplication.JointConditionalCountEntropy.sum_classSize_mul_empirical_entropy line 1199
  118. theorem OAI.MatrixAllFields.MatrixMultiplication.JointConditionalCountEntropy.sum_classSize_mul_entropy_of_law line 1214
  119. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupBranchLaws.jointCounts_branch_pos line 1249
  120. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupBranchLaws.branchLaw_stageA_mass_pos line 1260
  121. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupBranchLaws.branchLaw_stageB_mass_pos line 1266
  122. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupBranchLaws.supportedHalfLaw_branchShape_of_mass_pos line 1272
  123. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupBranchLaws.supportedHalfLaw_branchShape_of_mass_ne_zero line 1286
  124. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupBranchLaws.weighted_supportedHalfLaw_branchShape line 1297