OAI/NumberTheory/Ostmann/Characters/FrequencyExposure.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Ostmann.Characters.FrequencyExposure.Data line 11
  2. structure OAI.Ostmann.Characters.FrequencyExposure.Coefficients line 21
  3. def OAI.Ostmann.Characters.FrequencyExposure.constraint line 29
  4. def OAI.Ostmann.Characters.FrequencyExposure.update line 38
  5. def OAI.Ostmann.Characters.FrequencyExposure.reducedPair line 42
  6. def OAI.Ostmann.Characters.FrequencyExposure.budget line 45
  7. theorem OAI.Ostmann.Characters.FrequencyExposure.paired_frequency_tree_count line 51