OAI/Combinatorics/SumProduct/Alignment/TorusVertical01.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TorusVerticalFourier.finite_tests_of_dense_span line 35
  2. theorem OAI.TorusVerticalFourier.compact_superset_unit_lipschitz line 102
  3. lemma OAI.TorusVerticalFourier.character_add line 130
  4. lemma OAI.TorusVerticalFourier.character_cancel line 135
  5. def OAI.TorusVerticalFourier.coeff line 140
  6. lemma OAI.TorusVerticalFourier.coeff_apply line 149
  7. lemma OAI.TorusVerticalFourier.coeff_vadd line 154
  8. lemma OAI.TorusVerticalFourier.torus_coeff_unique line 170
  9. lemma OAI.TorusVerticalFourier.coeff_unique_at line 186
  10. def OAI.TorusVerticalFourier.HasWeight line 196
  11. lemma OAI.TorusVerticalFourier.coeff_hasWeight line 199
  12. lemma OAI.TorusVerticalFourier.hasWeight_one line 202
  13. lemma OAI.TorusVerticalFourier.HasWeight.mul line 207
  14. lemma OAI.TorusVerticalFourier.HasWeight.star line 214
  15. def OAI.TorusVerticalFourier.eigenfunctions line 222
  16. def OAI.TorusVerticalFourier.eigenAlgebra line 225
  17. lemma OAI.TorusVerticalFourier.eigenAlgebra_span line 234
  18. lemma OAI.TorusVerticalFourier.coeff_eval_eq line 244
  19. lemma OAI.TorusVerticalFourier.eigenAlgebra_separatesPoints line 261
  20. theorem OAI.TorusVerticalFourier.eigenfunctions_dense line 279
  21. lemma OAI.TorusVerticalFourier.coeff_lipschitz line 288
  22. lemma OAI.TorusVerticalFourier.lipschitz_mul line 315
  23. def OAI.TorusVerticalFourier.lipEigenfunctions line 334
  24. lemma OAI.TorusVerticalFourier.lipEigenfunctions_one line 338
  25. lemma OAI.TorusVerticalFourier.lipEigenfunctions_mul line 342
  26. lemma OAI.TorusVerticalFourier.lipEigenfunctions_star line 350
  27. def OAI.TorusVerticalFourier.lipEigenAlgebra line 357
  28. lemma OAI.TorusVerticalFourier.lipEigenAlgebra_span line 366
  29. lemma OAI.TorusVerticalFourier.lipEigenAlgebra_separatesPoints line 374
  30. theorem OAI.TorusVerticalFourier.lipEigenfunctions_dense line 397
  31. theorem OAI.TorusVerticalFourier.finite_vertical_obstruction_continuous line 406
  32. theorem OAI.TorusVerticalFourier.finite_vertical_obstruction line 424
  33. lemma OAI.TorusVerticalFourier.integral_hasWeight_eq_zero line 443
  34. def OAI.TorusVerticalFourier.balanced line 467
  35. lemma OAI.TorusVerticalFourier.balanced_invariant line 472
  36. abbrev OAI.TorusVerticalFourier.PairQuotient line 485
  37. def OAI.TorusVerticalFourier.balancedDescent line 490
  38. lemma OAI.TorusVerticalFourier.balancedDescent_apply line 502
  39. lemma OAI.TorusVerticalFourier.balanced_orbit_factorization line 507