OAI/NumberTheory/JointDickman/Amplification/CenteredBinSpectral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Full spectral bounds for the centered principal coefficient

  1. lemma OAI.JointDickman.centeredWeightedBinCoefficient_sub line 13
  2. theorem OAI.JointDickman.centered_bin_spectral line 27