OAI/Combinatorics/SumProduct/Alignment/FourierObstruction01.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FourierObstruction.finite_tests_of_dense_span line 21
  2. theorem OAI.FourierObstruction.compact_superset_unit_lipschitz line 88
  3. def OAI.FourierObstruction.discrepancy line 121
  4. theorem OAI.FourierObstruction.discrepancy_bound line 135
  5. theorem OAI.FourierObstruction.discrepancy_const line 145
  6. def OAI.FourierObstruction.torusHaar line 161
  7. instance OAI.FourierObstruction.torusHaar_probability line 163
  8. theorem OAI.FourierObstruction.integral_character line 166
  9. theorem OAI.FourierObstruction.torus_character_obstruction line 175
  10. def OAI.BracketHyperplanes.complexify line 210
  11. lemma OAI.BracketHyperplanes.torusHaar_eq_volume line 213
  12. lemma OAI.BracketHyperplanes.re_discrepancy line 216
  13. theorem OAI.BracketHyperplanes.finite_real_character_obstruction line 227
  14. lemma OAI.BracketHyperplanes.half_dense_mean line 258
  15. theorem OAI.BracketHyperplanes.compact_bracket_fourier line 274