OAI/Probability/SignedSweeps/ProvedRanges2.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.coefficientAction_eq_of_right_intertwines line 16
  2. def OAI.SignedSweeps.supportedCoefficients line 35
  3. lemma OAI.SignedSweeps.supportedCoefficients_action line 40
  4. lemma OAI.SignedSweeps.supportedCoefficients_positive line 48
  5. lemma OAI.SignedSweeps.supportedCoefficients_subgroup_action line 55
  6. theorem OAI.SignedSweeps.subgroup_supported_trace_bound line 77
  7. lemma OAI.SignedSweeps.finiteRegularRepresentation_norm line 102
  8. lemma OAI.SignedSweeps.finiteRegularRepresentation_single line 106
  9. lemma OAI.SignedSweeps.invariant_projection_diagonal line 113
  10. lemma OAI.SignedSweeps.invariant_projection_diagonal_trace line 123
  11. theorem OAI.SignedSweeps.invariant_evaluation_dimension_bound line 136
  12. lemma OAI.SignedSweeps.column_row_product_injective line 178
  13. lemma OAI.SignedSweeps.polytabloid_norm_sq line 193
  14. theorem OAI.SignedSweeps.spechtDimension_row_column_lower line 218
  15. def OAI.SignedSweeps.fiberPermEquiv line 230
  16. lemma OAI.SignedSweeps.card_fiberSubgroup line 248
  17. lemma OAI.SignedSweeps.fiber_product_injective line 253
  18. lemma OAI.SignedSweeps.card_fiber_product_le line 272
  19. lemma OAI.SignedSweeps.rowIndex_fiber_card line 279
  20. lemma OAI.SignedSweeps.colIndex_fiber_card line 301
  21. lemma OAI.SignedSweeps.card_rowSubgroup line 323
  22. lemma OAI.SignedSweeps.card_colSubgroup line 336
  23. lemma OAI.SignedSweeps.factorial_fiber_pair_bound line 359
  24. lemma OAI.SignedSweeps.row_removed_same_fiber line 381
  25. lemma OAI.SignedSweeps.row_removed_top_empty line 392
  26. lemma OAI.SignedSweeps.row_removal_factorial_product line 397
  27. lemma OAI.SignedSweeps.col_fiber_removal line 412
  28. lemma OAI.SignedSweeps.col_removal_factorial_product line 440
  29. theorem OAI.SignedSweeps.factorial_product_remove_full_row line 450
  30. lemma OAI.SignedSweeps.log_factorial_lower line 477
  31. lemma OAI.SignedSweeps.log_factorial_upper line 487
  32. lemma OAI.SignedSweeps.log_le_quarter_add_one line 505
  33. lemma OAI.SignedSweeps.Partition.rowColIndex_injective line 516
  34. lemma OAI.SignedSweeps.row_column_cell_sum_le line 523
  35. lemma OAI.SignedSweeps.row_column_entropy_sum_le line 540