OAI/Geometry/PeriodicTiling/PolynomialWeyl.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.scalarPhase line 17
  2. theorem OAI.PeriodicTilingThree.scalarPhase_zero line 20
  3. theorem OAI.PeriodicTilingThree.norm_scalarPhase line 23
  4. theorem OAI.PeriodicTilingThree.scalarPhase_add line 26
  5. theorem OAI.PeriodicTilingThree.scalarPhase_nat_mul line 30
  6. theorem OAI.PeriodicTilingThree.scalarPhase_sub line 37
  7. theorem OAI.PeriodicTilingThree.scalarPhase_ne_one_of_irrational line 44
  8. theorem OAI.PeriodicTilingThree.fourier_eq_scalarPhase line 55
  9. theorem OAI.PeriodicTilingThree.eval_degree_one line 59
  10. theorem OAI.PeriodicTilingThree.polynomial_phase_average_tendsto_zero line 67
  11. theorem OAI.PeriodicTilingThree.denseRange_circlePolynomial_of_irrational_leadingCoeff line 110