OAI/Analysis/IrrationalRotation/Model/ProductScales.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Invariant233.ProductScaleData line 11
  2. def OAI.Invariant233.ProductScaleData.prefixCount line 21
  3. def OAI.Invariant233.ProductScaleData.prefixCost line 24
  4. def OAI.Invariant233.ProductScaleData.coefficientBound line 27
  5. def OAI.Invariant233.ProductScaleData.kappa line 30
  6. def OAI.Invariant233.ProductScaleData.N line 32
  7. def OAI.Invariant233.ProductScaleData.a line 34
  8. def OAI.Invariant233.ProductScaleData.b line 36
  9. structure OAI.Invariant233.ProductScaleLaws line 42