OAI/NumberTheory/JointDickman/Amplification/LargeAlternativePairs.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.largeHighAlternativePairs line 12
2. theorem OAI.JointDickman.retained_addition_product line 24
3. theorem OAI.JointDickman.alternative_additions_subset_remainder line 36
4. theorem OAI.JointDickman.largeHighAlternativePairs_encoding line 44

   Source documentation

   Every actual pair maps to a fixed old-prime choice, a fixed opposite addition, and an element of the numerically sieved class.

   theorem largeHighAlternativePairs_encoding {B L k j d f : ℕ} {τ C Δ : ℝ}
       {A U D V X Y : Finset ℕ} (hk : k ∈ Icc 1 L)
       (hτ : 0 ≤ τ) (hℓ : 0 < auxiliaryLogLength B)
       (hA : A ⊆ auxiliaryPrimes B) (hU : U ⊆ auxiliaryPrimes B \ A)
       (hAr : RegularPrimeSet B L τ C A) (hUr : RegularPrimeSet B L τ C U)
       (hDr : RegularPrimeSet B L τ C D) (hVr : RegularPrimeSet B L τ C V)
       (hXY : (X,Y) ∈ largeHighAlternativePairs B L k j d f τ C Δ A U D V) :
       A \ X ∈ omissionEnvelope B L k τ A d ∧
       D \ Y ∈ omissionEnvelope B L k τ D f ∧
       Y \ D ∈ regularPrefixChoices B L k V f ∧
       X \ A ∈ (activeHighAdditionClass B L k τ C Δ A
         (∏ p ∈ A \ (A \ X), p) j
   …

   Mentions: OAI.JointDickman.auxiliaryLogLength, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.largeHighAlternativePairs, OAI.JointDickman.omissionEnvelope, OAI.JointDickman.regularPrefixChoices, OAI.JointDickman.activeHighAdditionClass