OAI/NumberTheory/JointDickman/Amplification/SmallCandidateMultiplicity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.smallCandidateAlternatives line 13
2. theorem OAI.JointDickman.smallCandidateAlternatives_subset line 19
3. def OAI.JointDickman.smallMultiplicityExponent line 32
4. theorem OAI.JointDickman.smallCandidateAlternatives_exp_bound line 35
5. theorem OAI.JointDickman.smallMultiplicityExponent_nonneg line 55
6. theorem OAI.JointDickman.smallCandidateAlternatives_rpow_bound line 64

   Source documentation

   The deterministic small-addition count has the same bound under every probability law on the two remainders.

   theorem smallCandidateAlternatives_rpow_bound {L : ℕ} (hL : 3 ≤ L)
       {τ : ℝ} (hτ : 0 < τ) (hτsmall : τ ≤ 1/100) :
       ∀ᶠ B : ℕ in atTop, ∀ (T H M : ℕ) (C : ℝ) (i k : Fin M) (A D U V : Finset ℕ),
         RegularPrimeSet B L τ C A → RegularPrimeSet B L τ C D →
         RegularPrimeSet B L τ C U → RegularPrimeSet B L τ C V →
         ((smallCandidateAlternatives B L T H τ C i k A D U V).card : ℝ) ≤
           (B : ℝ)^(smallMultiplicityExponent L τ) := by
   …

   Mentions: OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.smallCandidateAlternatives, OAI.JointDickman.smallMultiplicityExponent