OAI/Combinatorics/SquareDifference/GaussSum.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareDifference.IsSquareDifferenceFree line 13

    Also declared: ComparatorChallenges/SquareDifference.lean:7 (same declaration text).

  2. def OAI.SquareDifference.PowerSaving line 16
  3. lemma OAI.SquareDifference.gaussSum_norm_sq line 22
  4. lemma OAI.SquareDifference.square_sum_eq_gaussSum line 30
  5. lemma OAI.SquareDifference.square_sum_norm_sq line 52
  6. def OAI.SquareDifference.squareIndicator line 60
  7. lemma OAI.SquareDifference.squareIndicator_eq line 65
  8. lemma OAI.SquareDifference.squareIndicator_nonneg line 75
  9. lemma OAI.SquareDifference.squareIndicator_le_one line 81
  10. lemma OAI.SquareDifference.squareIndicator_sum line 87
  11. lemma OAI.SquareDifference.squareIndicator_char_sum line 99
  12. lemma OAI.SquareDifference.squareIndicator_char_sum_norm line 113
  13. lemma OAI.SquareDifference.dft_inner line 127
  14. lemma OAI.SquareDifference.dft_parseval line 150
  15. lemma OAI.SquareDifference.dft_convolution line 157
  16. lemma OAI.SquareDifference.convolution_l2_sq_le line 177
  17. lemma OAI.SquareDifference.centered_square_dft_bound line 195
  18. lemma OAI.SquareDifference.centered_square_convolution_l2 line 228
  19. lemma OAI.SquareDifference.single_square_mixing_unnormalized line 243
  20. lemma OAI.SquareDifference.single_square_mixing_bounded line 279
  21. lemma OAI.SquareDifference.expect_update line 312
  22. lemma OAI.SquareDifference.expect_update_two line 326
  23. lemma OAI.SquareDifference.single_square_mixing_expect line 335
  24. lemma OAI.SquareDifference.edge_product_factor line 344
  25. lemma OAI.SquareDifference.edge_product_abs_le_one line 370
  26. lemma OAI.SquareDifference.graph_edge_error line 376
  27. lemma OAI.SquareDifference.graph_counting line 423
  28. lemma OAI.SquareDifference.graph_count line 469
  29. lemma OAI.SquareDifference.four_cycle_bound line 478