OAI/LinearAlgebra/MatrixMultiplication/FieldGroups/NativeLaws.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Group assignments, orbit counts and extraction capacities.

  1. def OAI.MatrixMultiplication.AllFieldGroupNativeLaws.statisticComplement line 21
  2. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.childLaw_complementary_sides line 27
  3. def OAI.MatrixMultiplication.AllFieldGroupNativeLaws.halfLawAt line 41
  4. def OAI.MatrixMultiplication.AllFieldGroupNativeLaws.childWeight line 45
  5. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.halfLawAt_eq line 50
  6. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.halfLawAt_nonnegative line 58
  7. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.halfLawAt_normalized line 65
  8. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.halfLawAt_le_one_of_counts_pos line 73
  9. def OAI.MatrixMultiplication.AllFieldGroupNativeLaws.supportedHalfLaw line 83
  10. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.supportedHalfLaw_bounds line 87
  11. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.supportedHalfLaw_eq_of_counts_pos line 97
  12. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.placedLaw_mass_zero_of_count_zero line 106
  13. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.halfShape_childWeight line 116
  14. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.halfShape_mem_of_counts_pos line 124
  15. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.childWeight_sum line 133
  16. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.designated_source_geometry line 147
  17. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.compatibilityLaw_eq line 164
  18. def OAI.MatrixMultiplication.AllFieldGroupNativeLaws.nativePairLaw line 208
  19. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.placedLaw_sum_mul line 219
  20. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.childLaw_branchShape line 226
  21. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.rightChildLaw_branchShape line 234
  22. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.branchPairMixture_eq_native line 244
  23. def OAI.MatrixMultiplication.AllFieldGroupNativeLaws.placedPairMixture line 274
  24. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.placedPairMixture_eq_native line 278
  25. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.placement_symm_order_side line 286
  26. def OAI.MatrixMultiplication.AllFieldGroupNativeLaws.orderPairMixture line 293
  27. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.orderPairMixture_eq_native line 299
  28. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.orderPairMixture_supported line 307
  29. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.orderPairMixture_nonneg line 324
  30. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.orderPairMixture_total line 330
  31. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.orderPairMixture_entropy line 336
  32. def OAI.MatrixMultiplication.AllFieldGroupNativeLaws.nativeStatisticWeightCode line 345
  33. def OAI.MatrixMultiplication.AllFieldGroupNativeLaws.nativeSplitWeightCode line 351
  34. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.nativeSplitWeightCode_val line 355
  35. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.nativePairLaw_weight_marginal line 358
  36. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.commonWeight_law_ext line 377
  37. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.order_branch_weight line 387
  38. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.orderLaw_weight_marginal line 395
  39. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.orderPairLaw_common_weight line 414
  40. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.order_entropy_sub_pair_eq_conditional_sum line 421
  41. theorem OAI.MatrixMultiplication.AllFieldGroupNativeLaws.order_entropy_sub_mixture_eq_conditional_sum line 433