OAI/NumberTheory/JointDickman/Amplification/RegularAlternatives.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.regularSmallAlternatives line 10
2. theorem OAI.JointDickman.regularSmallAlternatives_omissions line 15
3. theorem OAI.JointDickman.regularSmallAlternatives_count line 42

   Source documentation

   Prefix membership and omitted higher primes determine an alternative uniquely. This preserves multiplicities without assuming disjoint first coefficient and remainder sets.

   theorem regularSmallAlternatives_count {B L k : ℕ} {τ C : ℝ}
       (A R : Finset ℕ) (hL : 1 ≤ L) (hk : k ∈ Icc 1 L)
       (hA : RegularPrimeSet B L τ C A) :
       (regularSmallAlternatives B L k τ C A R).card ≤
         2^(primePrefix B ((k : ℝ)/L) (A ∪ R)).card *
           (((A \ primePrefix B ((k : ℝ)/L) (A ∪ R)).powerset).filter
             (fun U => (U.card : ℝ) ≤ 4*τ*auxiliaryLogLength B)).card := by
   …

   Mentions: OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.regularSmallAlternatives, OAI.JointDickman.primePrefix, OAI.JointDickman.auxiliaryLogLength