OAI/LinearAlgebra/MatrixFields/Entropy/ZeroLeafRateFormula.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.entropyTerm line 18
2. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.finiteEntropy line 20
3. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.finiteEntropy_equiv line 22
4. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.entropyTerm_zero line 26
5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.entropyTerm_mul line 28
6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.finiteEntropy_chain line 38
7. structure OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw line 45
8. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.map line 54
9. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.map_mass line 66
10. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.map_mass_apply line 74
11. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.map_entropy_of_injective line 79
12. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.joint line 94
13. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.joint_entropy line 99
14. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.mass_le_map_mass line 104
15. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.conditional line 118
16. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.map_mass_mul_conditional line 127
17. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.entropy_eq_map_add_conditional line 147
18. inductive OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.EntropyDatum line 177
19. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.EntropyDatum.input line 181
20. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.EntropyDatum.output line 185
21. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.EntropyDatum.check line 189
22. lemma OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.EntropyDatum.sound line 193
23. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.entropyLookup line 210
24. lemma OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.entropyLookup_check line 213
25. lemma OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.entropyLookup_sound line 224
26. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.homogeneousEntropy line 246
27. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.homogeneousEntropy_normalized line 249
28. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.entropyTerm_divide line 254
29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.homogeneousEntropy_eq_mass_mul line 264
30. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.homogeneousEntropy_zero line 275
31. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.homogeneousEntropy_expansion line 279
32. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.entropyTerm_eq_negMulLog line 305
33. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.entropyTerm_one line 307
34. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.mul_entropyTerm_inv line 309
35. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.finiteEntropy_uniform line 317
36. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.finiteEntropy_deterministic line 323
37. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.continuous_entropyTerm line 330
38. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.entropyTerm_nonneg line 333
39. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.concaveOn_entropyTerm line 337
40. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.continuous_finiteEntropy line 340
41. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.tendsto_entropyTerm line 345
42. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.tendsto_entropyTerm_zero line 350
43. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.tendsto_finiteEntropy_of_tendsto line 355
44. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.finiteEntropy_nonneg line 361
45. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.finiteEntropy_mix_le line 365
46. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.finiteEntropy_le_log_card line 379
47. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.uniform line 409
48. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.uniform_mass line 417
49. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.uniform_entropy line 420
50. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.pure line 424
51. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.pure_entropy line 431
52. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.mass_le_one line 435
53. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.entropy_nonneg line 441
54. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.entropy_le_log_card line 444
55. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.map_entropy_le line 448
56. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.entropy_tendsto line 457
57. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLaw.map_mass_mul_conditional_map line 486
58. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.LabelRecord line 506
59. instance OAI.MatrixAllFields.MatrixMultiplication.Foundation.labelRecordFintype line 510
60. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.labelRecordOf line 520
61. structure OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy line 525
62. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.prefixLaw line 533
63. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.prefixLaw_zero_mass line 545
64. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.prefixLaw_succ line 549
65. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.prefixLaw_succ_mass line 555
66. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.refinementEntropy line 561
67. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.refinementEntropy_eq line 567
68. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.refinementEntropy_eq_zero_of_le line 574
69. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.zero_prefix_contribution line 579
70. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.prefixLaw_entropy_succ line 586
71. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.prefixLaw_entropy line 596
72. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.recordLaw line 607
73. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.recordLaw_entropy line 610
74. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.refinementEntropy_sum_of_injective_record line 615
75. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.ofLawLabels line 627
76. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.ofLawLabels_prefixLaw_mass line 631
77. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.ofLawLabels_refinementEntropy_eq line 655
78. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.ofLawLabels_refinementEntropy_sum line 665
79. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.FiniteLabelHierarchy.entropy_eq_sum_conditional_labels line 674
80. theorem OAI.MatrixAllFields.MatrixMultiplication.JointEntropyMax.entropy_nonneg line 707
81. theorem OAI.MatrixAllFields.MatrixMultiplication.JointEntropyMax.map_entropy_le line 711
82. theorem OAI.MatrixAllFields.MatrixMultiplication.JointEntropyMax.entropy_sub_map_nonneg line 716
83. theorem OAI.MatrixAllFields.MatrixMultiplication.JointEntropyMax.entropyTerm_le_crossEntropyTerm line 721
84. theorem OAI.MatrixAllFields.MatrixMultiplication.JointEntropyMax.entropy_le_crossEntropy line 735
85. theorem OAI.MatrixAllFields.MatrixMultiplication.JointEntropyMax.sum_mass_mul_coordinate line 746
86. theorem OAI.MatrixAllFields.MatrixMultiplication.JointEntropyMax.sum_mass_mul_coordinate_eq line 754
87. theorem OAI.MatrixAllFields.MatrixMultiplication.JointEntropyMax.entropy_le_of_three_marginals line 760
88. def OAI.MatrixAllFields.MatrixMultiplication.JointEntropyMax.normalizedPositiveLaw line 793
89. theorem OAI.MatrixAllFields.MatrixMultiplication.JointEntropyMax.normalizedPositiveLaw_mass_pos line 803
90. theorem OAI.MatrixAllFields.MatrixMultiplication.JointEntropyMax.entropy_le_normalized_product line 809
91. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroLeafRates.fourRate line 867