OAI/Combinatorics/SumProduct/Alignment/CharacterFactorization01.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CharacterFactorization.factorization_from_monomial_bounds line 39
  2. def OAI.RealCharacters.intScale line 92
  3. lemma OAI.RealCharacters.intScale_apply line 96
  4. lemma OAI.RealCharacters.intScale_continuous line 98
  5. lemma OAI.RealCharacters.intScale_ne_one line 102
  6. lemma OAI.RealCharacters.intScale_integral line 112
  7. lemma OAI.RealCharacters.intScale_kernel line 118
  8. lemma OAI.SquareHorizontalCharacter.diagonal_continuous line 139
  9. lemma OAI.SquareHorizontalCharacter.lower_continuous line 142
  10. lemma OAI.SquareHorizontalCharacter.diagonal_integral line 145
  11. lemma OAI.SquareHorizontalCharacter.lower_integral line 151
  12. lemma OAI.SquareHorizontalCharacter.lower_ne_one_of_diagonal line 157
  13. lemma OAI.SquareHorizontalCharacter.zero_pairing_kernel line 165
  14. lemma OAI.CharacterFactorization.lower_kernel_le line 178
  15. lemma OAI.CharacterFactorization.lower_kernel_lt line 181
  16. def OAI.CharacterFactorization.SmoothFactorizationAt line 210
  17. lemma OAI.CharacterFactorization.SmoothFactorizationAt.mono line 224
  18. theorem OAI.CharacterFactorization.finite_lower_factorizations line 244