OAI/Analysis/IrrationalRotation/Model/Fejer.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Invariant233.Fejer.Circle line 9
2. def OAI.Invariant233.Fejer.geometricPolynomial line 11
3. def OAI.Invariant233.Fejer.kernel line 14
4. def OAI.Invariant233.Fejer.frequencies line 17
5. def OAI.Invariant233.Fejer.coefficient line 19