OAI/Probability/Contingency/Signature.lean

GitHub source file

128 declarations, 0 contain sorry, 0 declared as axioms

Signature.

  1. theorem OAI.Contingency.sigPos_le_one_of_kernel line 22
  2. theorem OAI.Contingency.quadratic_add line 33
  3. theorem OAI.Contingency.sigPos_two_of_orthogonal_positive line 41
  4. theorem OAI.Contingency.positive_projection line 86
  5. def OAI.Contingency.pairForm line 110
  6. theorem OAI.Contingency.pairForm_apply line 119
  7. theorem OAI.Contingency.pairForm_first line 126
  8. theorem OAI.Contingency.pairForm_second line 131
  9. theorem OAI.Contingency.pairForm_both line 136
  10. theorem OAI.Contingency.pairForm_associated_first line 141
  11. theorem OAI.Contingency.pairForm_associated_second line 150
  12. theorem OAI.Contingency.pair_one line 160
  13. def OAI.Contingency.pairCumulative line 207
  14. theorem OAI.Contingency.pairCumulative_mul line 212
  15. theorem OAI.Contingency.pairCumulative_difference line 226
  16. def OAI.Contingency.pairPrevious line 236
  17. theorem OAI.Contingency.pair_sequence_one line 241
  18. theorem OAI.Contingency.discrete_laplacian_sum line 280
  19. theorem OAI.Contingency.pair_summation_signature line 295
  20. theorem OAI.Contingency.discrete_summation_by_parts line 321
  21. theorem OAI.Contingency.discrete_quadratic_weight line 344
  22. theorem OAI.Contingency.pair_summation_weighted line 359
  23. theorem OAI.Contingency.chain_product_telescope line 397
  24. def OAI.Contingency.IsLaminar line 448
  25. def OAI.Contingency.laminarCoefficient line 451
  26. theorem OAI.Contingency.laminar_blocks line 457
  27. def OAI.Contingency.matrixForm line 491
  28. theorem OAI.Contingency.matrixForm_apply line 495
  29. theorem OAI.Contingency.laminar_quadratic line 500
  30. theorem OAI.Contingency.laminarCoefficient_nonneg line 532
  31. theorem OAI.Contingency.laminar_matrix_signature line 540
  32. def OAI.Contingency.factorRemoval line 578
  33. def OAI.Contingency.factorRatio line 582
  34. def OAI.Contingency.factorGamma line 586
  35. theorem OAI.Contingency.factorRemoval_eq line 592
  36. def OAI.Contingency.truncatedFactorMatrix line 617
  37. theorem OAI.Contingency.truncated_laminar_signature line 623
  38. def OAI.Contingency.removePair line 670
  39. def OAI.Contingency.InBox line 673
  40. def OAI.Contingency.twoRemoval line 675
  41. def OAI.Contingency.HasSignature line 679
  42. def OAI.Contingency.PositiveSlice line 683
  43. theorem OAI.Contingency.sum_removePair line 688
  44. theorem OAI.Contingency.removePair_comm line 694
  45. theorem OAI.Contingency.removePair_inBox_iff line 700
  46. def OAI.Contingency.factorSlice line 729
  47. theorem OAI.Contingency.factorSlice_positive line 735
  48. theorem OAI.Contingency.factorSlice_signature line 747
  49. def OAI.Contingency.PosLogConcave line 770
  50. theorem OAI.Contingency.posLogConcave_of_convex_exponent line 773
  51. theorem OAI.Contingency.posLogConcave_abs line 782
  52. theorem OAI.Contingency.posLogConcave_positive_part line 790
  53. theorem OAI.Contingency.PosLogConcave.translate line 796
  54. theorem OAI.Contingency.PosLogConcave.reflect line 803
  55. theorem OAI.Contingency.posLogConcave_prod line 812
  56. def OAI.Contingency.groupedSequence line 827
  57. def OAI.Contingency.indexedFactorSlice line 830
  58. theorem OAI.Contingency.indexedFactorSlice_eq line 838
  59. theorem OAI.Contingency.indexedFactorSlice_signature line 860
  60. abbrev OAI.Contingency.Cell line 880
  61. abbrev OAI.Contingency.Coordinate line 881
  62. abbrev OAI.Contingency.FactorLabel line 882
  63. def OAI.Contingency.coordinateLine line 886
  64. def OAI.Contingency.softFactorSet line 889
  65. theorem OAI.Contingency.softFactorSet_laminar line 893
  66. def OAI.Contingency.softFactorExponent line 922
  67. def OAI.Contingency.softFactor line 931
  68. theorem OAI.Contingency.softFactor_logconcave line 935
  69. def OAI.Contingency.softPenalty line 968
  70. def OAI.Contingency.softWeight line 973
  71. theorem OAI.Contingency.softWeight_eq_factorSlice line 979
  72. theorem OAI.Contingency.softWeight_signature line 990
  73. theorem OAI.Contingency.softFactorSet_sum_row line 999
  74. theorem OAI.Contingency.softFactorSet_sum_col line 1007
  75. theorem OAI.Contingency.softPenalty_expansion line 1017
  76. def OAI.Contingency.pairAssembly line 1049
  77. theorem OAI.Contingency.pairAssembly_old line 1053
  78. theorem OAI.Contingency.pairAssembly_first line 1056
  79. theorem OAI.Contingency.pairAssembly_second line 1059
  80. def OAI.Contingency.pairAssemblyLinear line 1062
  81. theorem OAI.Contingency.signature_comp line 1073
  82. def OAI.Contingency.columnLinear line 1090
  83. theorem OAI.Contingency.columnLinear_apply line 1094
  84. theorem OAI.Contingency.matrixForm_pairAssembly line 1099
  85. def OAI.Contingency.removeOne line 1130
  86. theorem OAI.Contingency.pairAssembly_sum line 1134
  87. theorem OAI.Contingency.pairAssembly_inBox line 1139
  88. theorem OAI.Contingency.PositiveSlice.zero_of_negative line 1152
  89. theorem OAI.Contingency.removePair_pair_old line 1160
  90. theorem OAI.Contingency.removePair_pair_first line 1169
  91. theorem OAI.Contingency.removePair_pair_second line 1178
  92. theorem OAI.Contingency.removePair_pair_fresh line 1187
  93. def OAI.Contingency.pairQ line 1196
  94. def OAI.Contingency.pairS line 1200
  95. def OAI.Contingency.pairU line 1204
  96. theorem OAI.Contingency.pair_block_identity line 1209
  97. theorem OAI.Contingency.pairU_positive line 1260
  98. theorem OAI.Contingency.pairU_zero line 1272
  99. theorem OAI.Contingency.pairS_top line 1279
  100. theorem OAI.Contingency.pair_block_signature line 1289
  101. def OAI.Contingency.balancedMarginal line 1305
  102. theorem OAI.Contingency.matrixForm_sum line 1310
  103. theorem OAI.Contingency.balancedMarginal_signature line 1321
  104. theorem OAI.Contingency.balancedMarginal_positive line 1341
  105. theorem OAI.Contingency.actual_pair_weighted line 1367
  106. def OAI.Contingency.coordinatePullback line 1390
  107. theorem OAI.Contingency.removePair_reindex line 1396
  108. theorem OAI.Contingency.matrixForm_reindex line 1402
  109. theorem OAI.Contingency.HasSignature.reindex line 1415
  110. theorem OAI.Contingency.PositiveSlice.reindex line 1432
  111. def OAI.Contingency.rightCoordinates line 1450
  112. theorem OAI.Contingency.matrixForm_right line 1456
  113. theorem OAI.Contingency.removePair_fixed line 1463
  114. theorem OAI.Contingency.HasSignature.fixedContext line 1468
  115. theorem OAI.Contingency.PositiveSlice.fixedContext line 1489
  116. def OAI.Contingency.balanceBox line 1514
  117. def OAI.Contingency.balanceProfile line 1517
  118. def OAI.Contingency.balancedSlots line 1520
  119. def OAI.Contingency.splitSlot line 1524
  120. def OAI.Contingency.piHeadEquiv line 1538
  121. theorem OAI.Contingency.balanceBox_split line 1549
  122. theorem OAI.Contingency.balancedSlots_succ line 1559
  123. theorem OAI.Contingency.balancedSlots_closure line 1580
  124. theorem OAI.Contingency.softWeight_positive line 1620
  125. theorem OAI.Contingency.softWeight_context_balanced_signature line 1635
  126. theorem OAI.Contingency.softWeight_continuous line 1651
  127. theorem OAI.Contingency.softWeight_zero line 1662
  128. theorem OAI.Contingency.balancedSoft_continuous line 1679