OAI/NumberTheory/JointDickman/Amplification/BinWeightedMarginal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite-prime weights preserve the centered long mean

  1. def OAI.JointDickman.weightedCenteredBinPrefix line 12
  2. theorem OAI.JointDickman.centeredBin_divisor_prefix_tendsto line 18
  3. theorem OAI.JointDickman.weightedCenteredBinPrefix_tendsto line 47
  4. theorem OAI.JointDickman.weightedBinAverage_eq_prefix line 67
  5. theorem OAI.JointDickman.weightedBinAverage_long_tendsto line 92