OAI/NumberTheory/JointDickman/Arithmetic/DistinctBinDistribution.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Removing prime multiplicities in the finite-bin marginal law

  1. theorem OAI.JointDickman.primeBin_subset_allLarge line 11
  2. def OAI.JointDickman.distinctBinVector line 27
  3. theorem OAI.JointDickman.canonical_eq_distinctBinVector line 31
  4. theorem OAI.JointDickman.state_count_difference_bound line 46
  5. def OAI.JointDickman.distinctBinStateDensity line 68
  6. theorem OAI.JointDickman.binStateDensity_sub_distinct_tendsto line 71