OAI/Combinatorics/SumProduct/Alignment/PairTail05.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareInduction.discrepancy line 23
  2. theorem OAI.SquareInduction.discrepancy_bound line 37
  3. theorem OAI.SquareInduction.discrepancy_const line 47
  4. theorem OAI.SquareInduction.uniform_dense_square_descent_tracked line 65
  5. lemma OAI.SquareDifferences.norm_mean_derivative_swap line 150
  6. lemma OAI.SquareDifferences.derivative_shift_error line 159
  7. lemma OAI.SquareDifferences.nat_dist_image_card line 173
  8. theorem OAI.SquareDifferences.exists_dense_one_sided line 191
  9. def OAI.PairTail.diagonalEmbedding line 248
  10. def OAI.PairTail.lowerEmbedding line 252
  11. lemma OAI.PairTail.diagonalEmbedding_continuous line 256
  12. lemma OAI.PairTail.lowerEmbedding_continuous line 258
  13. lemma OAI.PairTail.pair_decompose line 261
  14. def OAI.PairTail.baseCharacter line 267
  15. def OAI.PairTail.lowerCharacter line 268
  16. lemma OAI.PairTail.baseCharacter_continuous line 269
  17. lemma OAI.PairTail.lowerCharacter_continuous line 271
  18. lemma OAI.PairTail.character_split line 275
  19. lemma OAI.PairTail.character_nonzero line 281
  20. lemma OAI.PairTail.lowerCharacter_conj line 293
  21. lemma OAI.PairTail.lower_commutator_mem line 305
  22. lemma OAI.PairTail.lowerCharacter_commutator line 309
  23. lemma OAI.PairTail.baseCharacter_integral line 320
  24. lemma OAI.PairTail.lowerCharacter_integral line 327