OAI/NumberTheory/JointDickman/Amplification/FirstRepresentationSum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.candidateSiteKernel_unrestricted_sum line 12

   Source documentation

   The unrestricted pair sum is exact: the coefficient and remainder weights themselves impose the four endpoint regularity conditions.

   theorem candidateSiteKernel_unrestricted_sum {B L T H M : ℕ} {τ C : ℝ}
       (χ : BlockCandidateIndex M → ℝ) (i t : Fin M) (hit : i < t)
       (S R : Finset ℕ) (hS : S ⊆ auxiliaryPrimes B) (hR : R ⊆ auxiliaryPrimes B) :
       candidateSiteKernel B L T H M τ C χ i t S R =
         ∑ ab ∈ (auxiliaryPrimes B).powerset.product (auxiliaryPrimes B).powerset,
           if BlockCandidateAdmissible B L T H τ C ((i,t),ab) ∧ ab.1 ⊆ S ∧ ab.2 ⊆ R then
             candidateCoefficientFactor B L τ C χ ((i,t),ab)*
               regularResidueWeight B L τ C (S \ ab.1)*regularResidueWeight B L τ C (R \ ab.2)
           else 0 := by
   …

   Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.candidateSiteKernel, OAI.JointDickman.BlockCandidateAdmissible, OAI.JointDickman.candidateCoefficientFactor, OAI.JointDickman.regularResidueWeight

2. theorem OAI.JointDickman.candidateSiteKernel_weighted_expectation line 65

   Source documentation

   Averaging after fixing the first pair produces exactly its tilted remainder law. The test can be the actual representation count.

   theorem candidateSiteKernel_weighted_expectation {B L T H M : ℕ} {τ C : ℝ}
       (χ : BlockCandidateIndex M → ℝ) (i t : Fin M) (hit : i < t)
       (F : Finset ℕ → Finset ℕ → ℝ) :
       (∑ S ∈ (auxiliaryPrimes B).powerset, ∑ R ∈ (auxiliaryPrimes B).powerset,
         bernoulliSubsetMass (auxiliaryPrimes B) (fun p => 1/(p : ℝ)) S*
         bernoulliSubsetMass (auxiliaryPrimes B) (fun p => 1/(p : ℝ)) R*F S R*
           candidateSiteKernel B L T H M τ C χ i t S R) =
       ∑ ab ∈ (auxiliaryPrimes B).powerset.product (auxiliaryPrimes B).powerset,
         if BlockCandidateAdmissible B L T H τ C ((i,t),ab) then
           candidateCoefficientFactor B L τ C χ ((i,t),ab)*
           (remainderTiltNormalizer B ab.1/(∏ p ∈ ab.1, p : ℕ))*
           (remainderTiltNormalizer B ab.2/(∏ p ∈ ab.2, p : ℕ))*
   …

   Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.candidateSiteKernel, OAI.JointDickman.BlockCandidateAdmissible, OAI.JointDickman.candidateCoefficientFactor, OAI.JointDickman.remainderTiltNormalizer