OAI/NumberTheory/JointDickman/Counting/CandidateCoefficientFactor.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.candidateCoefficientFactor line 10
2. theorem OAI.JointDickman.candidateCoefficientFactor_nonneg line 17
3. theorem OAI.JointDickman.candidateMeanWeight_factor line 27
4. theorem OAI.JointDickman.candidateCoefficientFactor_zero_left line 37
5. theorem OAI.JointDickman.candidateCoefficientFactor_zero_right line 45
6. theorem OAI.JointDickman.candidateSiteKernel_factor_sum line 57

   Source documentation

   The local site kernel is a sum of deterministic factors times the two regular remainder weights.

   theorem candidateSiteKernel_factor_sum {B L T H M : ℕ} {τ C : ℝ}
       (χ : BlockCandidateIndex M → ℝ) (i t : Fin M) (hit : i < t) (S R : Finset ℕ) :
       candidateSiteKernel B L T H M τ C χ i t S R =
         ∑ ab ∈ candidatePairRepresentations B L T H τ C i t S R,
           candidateCoefficientFactor B L τ C χ ((i,t),ab)*
             regularResidueWeight B L τ C (S \ ab.1)*regularResidueWeight B L τ C (R \ ab.2) := by
   …

   Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.candidateSiteKernel, OAI.JointDickman.candidatePairRepresentations, OAI.JointDickman.candidateCoefficientFactor, OAI.JointDickman.regularResidueWeight