OAI/NumberTheory/JointDickman/Amplification/AuxiliaryScalarBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Scalar bounds for summing the auxiliary logarithmic bins

  1. lemma OAI.JointDickman.auxiliary_threshold_bounds line 11
  2. lemma OAI.JointDickman.auxiliary_frequency_log line 23
  3. lemma OAI.JointDickman.auxiliary_exceptional_power line 35
  4. lemma OAI.JointDickman.eventually_auxiliary_log_lower line 55