OAI/Combinatorics/SharpThreshold/FourierBasis.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem313.BiasedFourier.scalarWeight line 15
  2. def OAI.Problem313.BiasedFourier.weight line 18
  3. def OAI.Problem313.BiasedFourier.chi line 21
  4. def OAI.Problem313.BiasedFourier.char line 24
  5. def OAI.Problem313.BiasedFourier.coeff line 27
  6. theorem OAI.Problem313.BiasedFourier.scalarWeight_false line 31
  7. theorem OAI.Problem313.BiasedFourier.scalarWeight_true line 32
  8. theorem OAI.Problem313.BiasedFourier.chi_false line 33
  9. theorem OAI.Problem313.BiasedFourier.chi_true line 35
  10. theorem OAI.Problem313.BiasedFourier.char_empty line 38
  11. theorem OAI.Problem313.BiasedFourier.scalar_kernel line 41
  12. theorem OAI.Problem313.BiasedFourier.character_kernel line 52
  13. theorem OAI.Problem313.BiasedFourier.inversion line 66
  14. theorem OAI.Problem313.BiasedFourier.parseval line 85
  15. theorem OAI.Problem313.BiasedFourier.coeff_zero line 109
  16. theorem OAI.Problem313.BiasedFourier.coeff_add line 114
  17. theorem OAI.Problem313.BiasedFourier.coeff_sub line 119
  18. theorem OAI.Problem313.BiasedFourier.coeff_smul line 124
  19. theorem OAI.Problem313.BiasedFourier.coeff_sum line 132
  20. theorem OAI.Problem313.BiasedFourier.inner_parseval line 139