OAI/NumberTheory/JointDickman/Amplification/MultiplicityParameters.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Choosing the grid and tolerance for the small-addition estimate

  1. theorem OAI.JointDickman.smallMultiplicityExponent_tendsto line 11
  2. theorem OAI.JointDickman.exists_small_multiplicity_tolerance line 20

    Source documentation

    The order is a fixed sufficiently fine grid, then a positive tolerance. No arithmetic or probabilistic premise is used in this choice.

    theorem exists_small_multiplicity_tolerance {L : ℕ} (hL : 10000 ≤ L) :
    ∃ τ : ℝ, 0 < τ ∧ τ ≤ samplingTau ∧ smallMultiplicityExponent L τ < 8/1000 := by
…

    Mentions: OAI.JointDickman.samplingTau, OAI.JointDickman.smallMultiplicityExponent

  3. theorem OAI.JointDickman.smallCandidateAlternatives_power_bound line 40