OAI/NumberTheory/Ostmann/Arithmetic/FrequencyModelCoefficients.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Fixed factors and ancestor coefficients of the frequency model

  1. def OAI.Ostmann.FrequencyModelState.leftProduct line 10
  2. def OAI.Ostmann.FrequencyModelState.rightProduct line 14
  3. def OAI.Ostmann.FrequencyModelState.compensation line 18
  4. def OAI.Ostmann.frequencyModelPivots line 22
  5. theorem OAI.Ostmann.frequencyModelAtPath_giants line 26
  6. theorem OAI.Ostmann.frequencyModelPivots_sources line 60
  7. theorem OAI.Ostmann.frequencyModelAtPath_products line 96
  8. def OAI.Ostmann.frequencyModelAncestorScheme line 124
  9. theorem OAI.Ostmann.frequencyModelNode_products line 132