OAI/NumberTheory/Ostmann/Construction/WordCharacterRemoval.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Repeat removal for the actual two-copy word statistic

  1. def OAI.Ostmann.wordCharacterEvent line 12
  2. theorem OAI.Ostmann.wordCharacterMean_eq_event_sum line 20
  3. def OAI.Ostmann.injectiveWordCharacterMean line 39
  4. theorem OAI.Ostmann.wordCopyPrimePrior line 47
  5. theorem OAI.Ostmann.word_character_repeat_removal line 58