OAI/NumberTheory/JointDickman/Amplification/FirstPairMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.candidateFirstPairMass line 12
2. theorem OAI.JointDickman.candidateFirstPairMass_term_le line 21

   Source documentation

   Domination of one first pair after its remainder laws are normalized.

   theorem candidateFirstPairMass_term_le {B L T H M : ℕ} {τ C : ℝ}
       (hB : 10 ≤ B) (hT : 0 < T) (hTs : (T : ℝ) ≤ Real.exp ((1/10 : ℝ)*B))
       (χ : BlockCandidateIndex M → ℝ) (i t : Fin M) (A D : Finset ℕ)
       (hA : A ⊆ auxiliaryPrimes B) (hD : D ⊆ auxiliaryPrimes B)
       (he : BlockCandidateAdmissible B L T H τ C ((i,t),(A,D))) (hχ : χ ((i,t),(A,D)) ≤ 1) :
       candidateCoefficientFactor B L τ C χ ((i,t),(A,D))*
         (remainderTiltNormalizer B A/(∏ p ∈ A, p : ℕ))*
         (remainderTiltNormalizer B D/(∏ p ∈ D, p : ℕ)) ≤
       (B : ℝ)*independentRootMean B L τ C*
         bernoulliSubsetMass (auxiliaryPrimes B) (fun p => (1/2 : ℝ)/p) A*
         bernoulliSubsetMass (auxiliaryPrimes B) (fun p => (1/2 : ℝ)/p) D*
         supportedEndpointTest B T (∏ p ∈ A, p) (t.val-i.val) (∏ p ∈ D, p) := by
   …

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