OAI/Combinatorics/SumProduct/Alignment/PairTail06.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PairTail.bracket line 30
  2. def OAI.PairTail.bracketCharacter line 32
  3. lemma OAI.PairTail.bracketCharacter_continuous line 47
  4. lemma OAI.PairTail.bracket_skew line 54
  5. def OAI.PairTail.leftBracketCharacter line 64
  6. lemma OAI.PairTail.leftBracketCharacter_apply line 66
  7. lemma OAI.PairTail.leftBracketCharacter_continuous line 69
  8. def OAI.PairTail.bracketMatrix line 75
  9. lemma OAI.PairTail.bracket_coordinates line 81
  10. lemma OAI.PairTail.bracketMatrix_skew line 103
  11. lemma OAI.PairTail.bracketMatrix_diagonal line 109
  12. theorem OAI.PairTail.integer_commutator_matrix line 117
  13. def OAI.PairTail.insideConj line 157
  14. lemma OAI.PairTail.lower_insideConj line 160
  15. lemma OAI.PairTail.bracket_inv_inv line 164
  16. def OAI.PairTail.normalizedTail line 172
  17. lemma OAI.PairTail.normalizedTail_val line 176
  18. lemma OAI.PairTail.lower_normalizedTail line 183
  19. def OAI.PairTail.normalizedPair line 192
  20. lemma OAI.PairTail.normalizedPair_val line 196
  21. lemma OAI.PairTail.normalizedPair_character line 203
  22. lemma OAI.PairTail.bracket_zpow line 217
  23. theorem OAI.PairTail.square_orbit_identity line 225
  24. lemma OAI.LeibmanSquare.linear_remainder_mem line 251
  25. def OAI.LeibmanSquare.linearRemainder line 274
  26. lemma OAI.LeibmanSquare.linearRemainder_mul line 277
  27. def OAI.LeibmanSquare.tailSquare line 282
  28. def OAI.LeibmanSquare.linearNormalizedPair line 288
  29. lemma OAI.LeibmanSquare.linearNormalizedPair_polynomial line 293
  30. lemma OAI.LeibmanSquare.linearNormalizedPair_val line 302
  31. lemma OAI.LeibmanSquare.linearNormalizedPair_reduced line 313
  32. lemma OAI.LeibmanSquare.balanced_linearNormalizedPair line 333
  33. lemma OAI.LeibmanSquare.linearNormalizedPair_eq_pairTail line 350