OAI/Analysis/IrrationalRotation/Model/CircleParameters.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Invariant233.CircleParameterData line 15
  2. def OAI.Invariant233.CircleParameterData.rep line 29
  3. def OAI.Invariant233.CircleParameterData.delta line 31
  4. def OAI.Invariant233.CircleParameterData.kernelWidth line 33
  5. def OAI.Invariant233.CircleParameterData.kernel line 35
  6. def OAI.Invariant233.CircleParameterData.orientedKernel line 39
  7. def OAI.Invariant233.CircleParameterData.blockEnd line 42
  8. def OAI.Invariant233.CircleParameterData.blockIndex line 45
  9. def OAI.Invariant233.CircleParameterData.flattenedFrequency line 49
  10. def OAI.Invariant233.CircleParameterData.flattenedCost line 51
  11. def OAI.Invariant233.CircleParameterData.block line 54
  12. def OAI.Invariant233.CircleParameterData.N line 57
  13. def OAI.Invariant233.CircleParameterData.a line 59
  14. def OAI.Invariant233.CircleParameterData.b line 61
  15. def OAI.Invariant233.CircleParameterData.Q line 63
  16. def OAI.Invariant233.CircleParameterData.kappa line 66
  17. def OAI.Invariant233.CircleParameterData.alpha line 68
  18. def OAI.Invariant233.CircleParameterData.coordinate line 71
  19. def OAI.Invariant233.CircleParameterData.ell line 74
  20. def OAI.Invariant233.CircleParameterData.shift line 78
  21. def OAI.Invariant233.CircleParameterData.coefficientBound line 81
  22. def OAI.Invariant233.CircleParameterData.convolutionCoefficient line 85
  23. def OAI.Invariant233.CircleParameterData.samplingAverage line 88
  24. structure OAI.Invariant233.CircleParameterLaws line 99