OAI/Combinatorics/Sidorenko/SignMoments.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SidorenkoCounterexample.char_conj line 15
  2. theorem OAI.SidorenkoCounterexample.character_differencing line 19
  3. theorem OAI.SidorenkoCounterexample.linear_character_sum_zero line 33
  4. theorem OAI.SidorenkoCounterexample.quadratic_difference line 54

    Source documentation

    Exact one-step differencing for a symmetric quadratic polynomial.

     theorem quadratic_difference (B : LinearMap.BilinForm K V) (hB : B.IsSymm)
    (l : V →ₗ[K] K) (c : K) (z u : V) :
    (B (z+u) (z+u) + l (z+u) + c) - (B z z + l z + c) =
      B u u + l u + (2 : K) * B u z := by
…
  5. theorem OAI.SidorenkoCounterexample.quadratic_gauss_bound line 63

    Source documentation

    The raw quadratic Gauss bound, with arbitrary linear and constant terms. Its right side is exactly |V| times the size of the radical.

     theorem quadratic_gauss_bound (ψ : AddChar K ℂ) (hψ : ψ ≠ 0)
    (hodd : (2 : K) ≠ 0) (B : LinearMap.BilinForm K V) (hB : B.IsSymm)
    (l : V →ₗ[K] K) (c : K) :
    ‖∑ x, ψ (B x x + l x + c)‖ ^ 2 ≤
      (Fintype.card V : ℝ) * Nat.card B.ker := by
…
  6. theorem OAI.SidorenkoCounterexample.normalized_quadratic_gauss_bound line 100
  7. def OAI.SidorenkoCounterexample.coordinatePairing line 130
  8. theorem OAI.SidorenkoCounterexample.coordinate_character_sum line 135
  9. def OAI.SidorenkoCounterexample.finiteFourier line 149
  10. theorem OAI.SidorenkoCounterexample.finite_parseval line 152
  11. theorem OAI.SidorenkoCounterexample.finiteFourier_sub_uniform line 179
  12. theorem OAI.SidorenkoCounterexample.finite_fourier_l1_bound line 198
  13. theorem OAI.SidorenkoCounterexample.finite_fourier_l1_of_uniform_bound line 213
  14. def OAI.SidorenkoCounterexample.uniformLaw line 232
  15. theorem OAI.SidorenkoCounterexample.uniformLaw_sum line 236
  16. theorem OAI.SidorenkoCounterexample.uniformLaw_average line 243
  17. theorem OAI.SidorenkoCounterexample.finiteFourier_uniformLaw line 254
  18. def OAI.SidorenkoCounterexample.quadraticMap line 269
  19. theorem OAI.SidorenkoCounterexample.quadraticMap_frequency line 274
  20. theorem OAI.SidorenkoCounterexample.quadraticMap_fourier_bound line 280
  21. theorem OAI.SidorenkoCounterexample.quadraticMap_joint_l1_bound line 298
  22. def OAI.SidorenkoCounterexample.characterProduct line 329
  23. theorem OAI.SidorenkoCounterexample.characterProduct_abs_le line 332
  24. theorem OAI.SidorenkoCounterexample.characterProduct_sum line 340
  25. theorem OAI.SidorenkoCounterexample.bounded_test_l1 line 350
  26. theorem OAI.SidorenkoCounterexample.quadraticMap_character_moment line 364
  27. theorem OAI.SidorenkoCounterexample.matrix_form_rank line 402
  28. theorem OAI.SidorenkoCounterexample.schur_polynomial line 408
  29. theorem OAI.SidorenkoCounterexample.inverse_form_span_rank line 421
  30. theorem OAI.SidorenkoCounterexample.schur_sign_moment line 434
  31. theorem OAI.SidorenkoCounterexample.matrix_combination_form_rank line 488
  32. theorem OAI.SidorenkoCounterexample.matrix_low_rank_span_bound line 506
  33. def OAI.SidorenkoCounterexample.goodMinors line 528
  34. def OAI.SidorenkoCounterexample.minorBadBound line 532
  35. theorem OAI.SidorenkoCounterexample.badMinors_bound line 535
  36. def OAI.SidorenkoCounterexample.starDifference line 600
  37. theorem OAI.SidorenkoCounterexample.starDifference_surjective line 605
  38. theorem OAI.SidorenkoCounterexample.uniformMean_starDifference line 617
  39. theorem OAI.SidorenkoCounterexample.symmetricBorder_sub line 627
  40. theorem OAI.SidorenkoCounterexample.uniformMean_pi_prod line 636
  41. theorem OAI.SidorenkoCounterexample.uniformMean_bordered line 644