OAI/NumberTheory/JointDickman/Amplification/BinStateExtraction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Extracting finite-state probabilities from generating values

  1. theorem OAI.JointDickman.exists_bounded_real_count_interpolation line 10
  2. def OAI.JointDickman.binStateGeneratingAverage line 20
  3. theorem OAI.JointDickman.binStateDensity_interpolation line 23
  4. theorem OAI.JointDickman.binStateDensity_sum line 44
  5. theorem OAI.JointDickman.binStateDistribution_of_generating_limits line 51