OAI/Probability/SignedSweeps/BaseCases.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.partition_mem_bounds line 10
  2. instance OAI.SignedSweeps.partitionFinite line 22
  3. lemma OAI.SignedSweeps.rowOf_eq_zero line 33
  4. lemma OAI.SignedSweeps.rowSubgroup_eq_top line 41
  5. lemma OAI.SignedSweeps.colSubgroup_eq_bot line 47
  6. def OAI.SignedSweeps.regularOnes line 62
  7. lemma OAI.SignedSweeps.regularOnes_apply line 65
  8. lemma OAI.SignedSweeps.regularOnes_ne_zero line 67
  9. lemma OAI.SignedSweeps.regularOnes_invariant line 72
  10. lemma OAI.SignedSweeps.polytabloid_row line 77
  11. lemma OAI.SignedSweeps.spechtSubrepresentation_row line 99
  12. lemma OAI.SignedSweeps.spechtDimension_row line 111
  13. lemma OAI.SignedSweeps.spechtRepresentation_row line 117
  14. lemma OAI.SignedSweeps.layerOperator_row line 128
  15. lemma OAI.SignedSweeps.sweepOperator_row line 135
  16. lemma OAI.SignedSweeps.weightedMoment_row line 140
  17. lemma OAI.SignedSweeps.finite_base_moments line 146