OAI/Probability/SignedSweeps/RestrictionSum.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.mixedConjugationSum line 17
  2. lemma OAI.SignedSweeps.mixedConjugationSum_intertwines line 20
  3. lemma OAI.SignedSweeps.matrixCoefficient_inner_eq_zero line 37
  4. lemma OAI.SignedSweeps.bilateral_matrixCoefficient line 59
  5. lemma OAI.SignedSweeps.subgroup_coefficient_orthogonal line 70
  6. lemma OAI.SignedSweeps.subgroupCoefficientProjection_kills line 85
  7. lemma OAI.SignedSweeps.supportedCoefficients_kills line 106
  8. lemma OAI.SignedSweeps.coefficientAction_sub line 120
  9. lemma OAI.SignedSweeps.supportedCoefficients_difference_positive line 126
  10. lemma OAI.SignedSweeps.supportedCoefficients_trace_le line 147
  11. def OAI.SignedSweeps.RestrictionEligible line 170
  12. theorem OAI.SignedSweeps.specht_positive_restriction line 174
  13. def OAI.SignedSweeps.outerTensorRepresentation line 222
  14. lemma OAI.SignedSweeps.outerTensorRepresentation_apply line 229
  15. lemma OAI.SignedSweeps.outerTensorRepresentation_norm line 234
  16. lemma OAI.SignedSweeps.outerTensorRepresentation_character line 244
  17. lemma OAI.SignedSweeps.outerTensorRepresentation_end_finrank line 252
  18. theorem OAI.SignedSweeps.outerTensorRepresentation_irreducible line 284
  19. theorem OAI.SignedSweeps.exists_specht_intertwiner line 306
  20. def OAI.SignedSweeps.multiplicityAction line 337
  21. lemma OAI.SignedSweeps.multiplicityAction_apply line 348
  22. def OAI.SignedSweeps.multiplicityRepresentation line 353
  23. lemma OAI.SignedSweeps.multiplicityRepresentation_apply line 371
  24. def OAI.SignedSweeps.tensorMultiplicityEvaluation line 376
  25. lemma OAI.SignedSweeps.tensorMultiplicityEvaluation_tmul line 388
  26. def OAI.SignedSweeps.tensorMultiplicityIntertwiner line 393
  27. lemma OAI.SignedSweeps.tensorMultiplicityIntertwiner_ne_zero line 410
  28. theorem OAI.SignedSweeps.exists_external_specht_extension line 433
  29. lemma OAI.SignedSweeps.complexSign_norm line 466
  30. def OAI.SignedSweeps.signTwist line 471
  31. lemma OAI.SignedSweeps.signTwist_norm line 477
  32. def OAI.SignedSweeps.orbitEvaluation line 483
  33. lemma OAI.SignedSweeps.orbitEvaluation_intertwines line 489
  34. lemma OAI.SignedSweeps.orbitEvaluation_single line 499
  35. lemma OAI.SignedSweeps.orbitEvaluation_polytabloid line 504
  36. lemma OAI.SignedSweeps.projection_product_nonzero line 524
  37. def OAI.SignedSweeps.spechtOrbitIntertwiner line 535
  38. theorem OAI.SignedSweeps.specht_occurs_of_row_average line 541