OAI/NumberTheory/JointDickman/Arithmetic/DistinctBinGenerating.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Generating functions are unchanged by discarding repeated large primes

  1. theorem OAI.JointDickman.distinctBinCount_le_binCount line 11
  2. theorem OAI.JointDickman.distinctBinVector_val line 23
  3. def OAI.JointDickman.distinctBinGeneratingAverage line 33
  4. theorem OAI.JointDickman.binStateGeneratingAverage_states line 36
  5. theorem OAI.JointDickman.distinctBinGeneratingAverage_states line 46
  6. theorem OAI.JointDickman.binGenerating_sub_distinct_tendsto line 56