OAI/Probability/SignedSweeps/Model.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SignedSweeps.Partition line 10

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:11 (same declaration text).

  2. abbrev OAI.SignedSweeps.SymmetricGroup line 12

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:13 (same declaration text).

  3. def OAI.SignedSweeps.Partition.transpose line 22

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:17 (same declaration text).

  4. def OAI.SignedSweeps.Partition.tableau line 25

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:20 (same declaration text).

  5. def OAI.SignedSweeps.Partition.rowOf line 28

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:23 (same declaration text).

  6. def OAI.SignedSweeps.Partition.colOf line 31

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:26 (same declaration text).

  7. def OAI.SignedSweeps.fiberSubgroup line 42

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:31 (same declaration text).

  8. def OAI.SignedSweeps.rowSubgroup line 52

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:41 (same declaration text).

  9. def OAI.SignedSweeps.colSubgroup line 55

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:44 (same declaration text).

  10. abbrev OAI.SignedSweeps.RegularSpace line 58

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:47 (same declaration text).

  11. def OAI.SignedSweeps.regularIsometry line 60

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:49 (same declaration text).

  12. lemma OAI.SignedSweeps.regularIsometry_apply line 65

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:54 (same declaration text).

  13. def OAI.SignedSweeps.regularRepresentation line 69

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:58 (same declaration text).

  14. lemma OAI.SignedSweeps.regularRepresentation_apply line 78

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:67 (same declaration text).

  15. def OAI.SignedSweeps.polytabloid line 82

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:71 (same declaration text).

  16. def OAI.SignedSweeps.spechtSubrepresentation line 88

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:77 (same declaration text).

  17. def OAI.SignedSweeps.Specht line 105

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:94 (same declaration text).

  18. instance OAI.SignedSweeps.spechtNormedAddCommGroup line 107

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:96 (same declaration text).

  19. instance OAI.SignedSweeps.spechtInnerProductSpace line 110

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:99 (same declaration text).

  20. instance OAI.SignedSweeps.spechtFiniteDimensional line 113

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:102 (same declaration text).

  21. def OAI.SignedSweeps.spechtRepresentation line 116

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:105 (same declaration text).

  22. def OAI.SignedSweeps.spechtDimension line 120

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:109 (same declaration text).

  23. def OAI.SignedSweeps.blockEmbedding line 122

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:111 (same declaration text).

  24. def OAI.SignedSweeps.SignedOccurrence line 130

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:119 (same declaration text).

  25. abbrev OAI.SignedSweeps.BinaryPositions line 140

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:129 (same declaration text).

  26. def OAI.SignedSweeps.positionsEquiv line 142

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:131 (same declaration text).

  27. def OAI.SignedSweeps.coordinateSubgroup line 145

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:134 (same declaration text).

  28. def OAI.SignedSweeps.layerOperator line 149

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:138 (same declaration text).

  29. def OAI.SignedSweeps.sweepOperator line 155

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:144 (same declaration text).

  30. def OAI.SignedSweeps.positiveSquare line 158

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:147 (same declaration text).

  31. def OAI.SignedSweeps.sweepSquare line 161

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:150 (same declaration text).

  32. def OAI.SignedSweeps.weightedMoment line 164

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:153 (same declaration text).

  33. def OAI.SignedSweeps.logMoment line 167

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:156 (same declaration text).

  34. def OAI.SignedSweeps.signedEntropy line 169

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:158 (same declaration text).

  35. def OAI.SignedSweeps.coefficient line 173

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:162 (same declaration text).

  36. def OAI.SignedSweeps.remainderBudget line 175

    Also declared: ComparatorChallenges/SignedSweepMoment.lean:164 (same declaration text).

  37. lemma OAI.SignedSweeps.positive_pow line 180
  38. lemma OAI.SignedSweeps.adjoint_mul_positive line 190
  39. lemma OAI.SignedSweeps.sweepSquare_positive line 194
  40. lemma OAI.SignedSweeps.sweepSquare_pow_positive line 198
  41. lemma OAI.SignedSweeps.sweepSquare_pow_trace_real line 202
  42. lemma OAI.SignedSweeps.weightedMoment_nonneg line 207
  43. lemma OAI.SignedSweeps.weightedMoment_zero_power line 212
  44. lemma OAI.SignedSweeps.logMoment_zero line 217
  45. lemma OAI.SignedSweeps.logMoment_pos line 219
  46. lemma OAI.SignedSweeps.logMoment_le_iff line 222
  47. lemma OAI.SignedSweeps.row_part_le_size line 229
  48. lemma OAI.SignedSweeps.signedEntropy_nonneg line 234
  49. lemma OAI.SignedSweeps.signedEntropy_empty line 252
  50. lemma OAI.SignedSweeps.coefficient_bounds line 267
  51. lemma OAI.SignedSweeps.coefficient_nonneg line 278
  52. lemma OAI.SignedSweeps.remainderBudget_zero line 283
  53. lemma OAI.SignedSweeps.remainderBudget_nonneg line 286
  54. lemma OAI.SignedSweeps.entropy_angle_tradeoff line 290
  55. lemma OAI.SignedSweeps.spechtRepresentation_norm line 299
  56. lemma OAI.SignedSweeps.finite_average_contraction line 305
  57. lemma OAI.SignedSweeps.layerOperator_contraction line 322
  58. lemma OAI.SignedSweeps.list_prod_contraction line 329
  59. lemma OAI.SignedSweeps.sweepOperator_contraction line 338
  60. lemma OAI.SignedSweeps.adjoint_contraction line 346
  61. lemma OAI.SignedSweeps.contraction_pow line 360
  62. lemma OAI.SignedSweeps.sweepSquare_contraction line 369
  63. lemma OAI.SignedSweeps.contraction_trace_le_dim line 375
  64. lemma OAI.SignedSweeps.weightedMoment_le_dimension_squared line 390
  65. lemma OAI.SignedSweeps.polytabloid_empty line 397
  66. lemma OAI.SignedSweeps.polytabloid_empty_ne_zero line 407
  67. lemma OAI.SignedSweeps.spechtSubrepresentation_empty line 413
  68. lemma OAI.SignedSweeps.spechtDimension_empty line 426