CandidateScalarIdentity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Identifying the arithmetic scalar with an admissible candidate

theorem OAI.JointDickman.candidateQuotient_of_relation line 14
Source documentation
The candidate quotient is the unique coefficient in its additive relation.
```
theorem candidateQuotient_of_relation {M : ℕ} {e : BlockCandidateIndex M} {c : ℕ}
    (hj : 0 < candidateLag e)
    (he : candidateHigh e = candidateLow e+candidateLag e*c) :
    candidateQuotient e = c := by
…
```
Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.candidateLag, OAI.JointDickman.candidateHigh, OAI.JointDickman.candidateLow, OAI.JointDickman.candidateQuotient
theorem OAI.JointDickman.amplificationScalarWeight_support line 22

theorem OAI.JointDickman.candidateAdmissible_of_scalar line 65

Source documentation

Once the three retained coefficients are regular and the endpoints are coprime, every nonzero smooth arithmetic summand is an actual candidate.

theorem candidateAdmissible_of_scalar {B L T H M c : ℕ} {τ C : ℝ}
    (hB : 0 < B) (hT : 0 < T) (hc : 0 < c)
    {i t : Fin M} (hit : i < t) {A D : Finset ℕ}
    (hH : H < t.val-i.val) (hjT : t.val-i.val < T)
    (hw : amplificationScalarWeight B (t.val-i.val) T c
      (∏ p ∈ A,p) (∏ p ∈ D,p) ≠ 0)
    (hcop : (∏ p ∈ A,p).Coprime (∏ p ∈ D,p))
    (hreg : RegularPrimeSet B L τ C (coefficientPrimeSet B c)) :
    BlockCandidateAdmissible B L T H τ C ((i,t),(A,D)) := by
…

Mentions: OAI.JointDickman.amplificationScalarWeight, OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.coefficientPrimeSet, OAI.JointDickman.BlockCandidateAdmissible

def OAI.JointDickman.regularCandidateScalar line 90

theorem OAI.JointDickman.regularCandidateScalar_eq_of_relation line 100

Source documentation

The candidate restrictions impose no extra condition on a nonzero smooth summand once coprimality and coefficient regularity are retained.

theorem regularCandidateScalar_eq_of_relation {B L T H M c : ℕ} {τ C : ℝ}
    (hB : 0 < B) (hT : 0 < T) (hc : 0 < c)
    {i t : Fin M} (hit : i < t) {A D : Finset ℕ}
    (hH : H < t.val-i.val) (hjT : t.val-i.val < T)
    (he : (∏ p ∈ D,p) = (∏ p ∈ A,p)+(t.val-i.val)*c) :
    regularCandidateScalar B L T H τ C ((i,t),(A,D)) =
      if (∏ p ∈ A,p).Coprime (∏ p ∈ D,p) ∧
          RegularPrimeSet B L τ C (coefficientPrimeSet B c) then
        amplificationScalarWeight B (t.val-i.val) T c (∏ p ∈ A,p) (∏ p ∈ D,p)
      else 0 := by
…

Mentions: OAI.JointDickman.regularCandidateScalar, OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.coefficientPrimeSet, OAI.JointDickman.amplificationScalarWeight