OAI/Probability/SignedSweeps/ProvedRanges3.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.spechtDimension_positive line 12
  2. lemma OAI.SignedSweeps.spechtDimension_factorial_lower line 15
  3. theorem OAI.SignedSweeps.specht_log_dimension_small_axes line 25
  4. lemma OAI.SignedSweeps.Partition.firstRow_pos line 51
  5. lemma OAI.SignedSweeps.Partition.firstCol_pos line 55
  6. lemma OAI.SignedSweeps.Partition.firstRow_le line 59
  7. lemma OAI.SignedSweeps.factorial_product_remove_first_row line 67
  8. lemma OAI.SignedSweeps.column_log_sum_le line 90
  9. lemma OAI.SignedSweeps.log_degree_from_first_row line 106
  10. lemma OAI.SignedSweeps.Partition.firstCol_le line 141
  11. lemma OAI.SignedSweeps.deficit_log_ratio_lower line 146
  12. lemma OAI.SignedSweeps.log_degree_long_first_row line 156
  13. theorem OAI.SignedSweeps.specht_log_dimension_deficit line 177
  14. lemma OAI.SignedSweeps.nonsparse_degree_error line 232
  15. theorem OAI.SignedSweeps.nonsparse_specht_log_dimension line 265
  16. theorem OAI.SignedSweeps.nonsparse_signed_entropy_size line 275
  17. theorem OAI.SignedSweeps.nonsparse_closing_budget line 296
  18. def OAI.SignedSweeps.assignmentBlock line 331
  19. lemma OAI.SignedSweeps.assignmentBlock_mul line 334
  20. lemma OAI.SignedSweeps.trace_blockDiagonal'_mul line 355
  21. theorem OAI.SignedSweeps.labeled_assignment_trace line 374
  22. abbrev OAI.SignedSweeps.HoleAssignment line 396
  23. def OAI.SignedSweeps.holeColumns line 398
  24. def OAI.SignedSweeps.holeRows line 401
  25. lemma OAI.SignedSweeps.hole_rows_columns_injective line 404
  26. theorem OAI.SignedSweeps.labeled_hole_trace line 411
  27. lemma OAI.SignedSweeps.nonnegative_prod_le_mean_power line 421
  28. def OAI.SignedSweeps.missingLineFactor line 451
  29. lemma OAI.SignedSweeps.missingLineFactor_nonneg line 453
  30. lemma OAI.SignedSweeps.missingLineFactor_empty line 457
  31. lemma OAI.SignedSweeps.missingLineFactor_le_exp line 460
  32. def OAI.SignedSweeps.occupiedRow line 479
  33. def OAI.SignedSweeps.missingCellFactor line 482
  34. lemma OAI.SignedSweeps.sum_occupiedRow_card line 485
  35. theorem OAI.SignedSweeps.occupied_cell_product_bound line 491