OAI/NumberTheory/JointDickman/Amplification/SignedProductGcd.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.primeProductMass_pair_sum_test line 14
2. theorem OAI.JointDickman.halfPrimeProduct_bad_pair_mass line 33
3. theorem OAI.JointDickman.signedPrimeProductPair_coprime_error line 66
4. theorem OAI.JointDickman.amplificationFairKernel_product_expectation line 127

   Source documentation

   The product weight sums the unique additive coefficient before the two endpoint laws are pushed forward.

   theorem amplificationFairKernel_product_expectation (B j : ℕ) (T : ℝ) (V : ℕ)
       (g h : (auxiliaryPrimes B → Bool) → ℝ) :
       (∑ x : auxiliaryPrimes B → Bool, ∑ z : auxiliaryPrimes B → Bool,
         fullPrimeMass (auxiliaryPrimes B) x*fullPrimeMass (auxiliaryPrimes B) z*g x*h z*
           amplificationFairKernel B j T V x z) =
       ∑ a ∈ primeSplitProductSupport (auxiliaryPrimes B),
         ∑ b ∈ primeSplitProductSupport (auxiliaryPrimes B),
           signedSplitProductMass (auxiliaryPrimes B) (subsetSiteTest (auxiliaryPrimes B) g) a*
             signedSplitProductMass (auxiliaryPrimes B) (subsetSiteTest (auxiliaryPrimes B) h) b*
               amplificationProductWeight B j T V a b := by
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.fullPrimeMass, OAI.JointDickman.amplificationFairKernel, OAI.JointDickman.primeSplitProductSupport, OAI.JointDickman.signedSplitProductMass, OAI.JointDickman.subsetSiteTest, OAI.JointDickman.amplificationProductWeight

5. theorem OAI.JointDickman.amplification_product_coprime_error line 160

   Source documentation

   The actual smooth amplification weight satisfies the finite gcd-removal estimate.

   theorem amplification_product_coprime_error {B j : ℕ} (hB : 0 < B) (hj : 0 < j)
       (T : ℝ) (V : ℕ) (g h : (auxiliaryPrimes B → Bool) → ℝ)
       (hg : ∀ x, |g x| ≤ 1) (hh : ∀ x, |h x| ≤ 1) :
       |(∑ a ∈ primeSplitProductSupport (auxiliaryPrimes B),
           ∑ b ∈ primeSplitProductSupport (auxiliaryPrimes B),
         signedSplitProductMass (auxiliaryPrimes B) (subsetSiteTest (auxiliaryPrimes B) g) a*
         signedSplitProductMass (auxiliaryPrimes B) (subsetSiteTest (auxiliaryPrimes B) h) b*
           amplificationProductWeight B j T V a b)-
         (∑ a ∈ primeSplitProductSupport (auxiliaryPrimes B),
           ∑ b ∈ primeSplitProductSupport (auxiliaryPrimes B),
           if a.Coprime b then
             signedSplitProductMass (auxiliaryPrimes B) (subsetSiteTest (auxiliaryPrimes B) g) a*
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.primeSplitProductSupport, OAI.JointDickman.signedSplitProductMass, OAI.JointDickman.subsetSiteTest, OAI.JointDickman.amplificationProductWeight

6. theorem OAI.JointDickman.amplification_gcd_rate_tendsto line 184