OAI/NumberTheory/JointDickman/Amplification/BinStateLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Existence of the unconditional finite-bin state distribution

  1. theorem OAI.JointDickman.distinctBinGeneratingAverage_tendsto line 12
  2. theorem OAI.JointDickman.binStateGeneratingAverage_tendsto line 36
  3. theorem OAI.JointDickman.finiteBinStateDistribution line 44