ArithmeticCandidateWeight.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The six arithmetic graph factors are the candidate root weight

def OAI.JointDickman.candidateCutoff line 12

theorem OAI.JointDickman.arithmetic_graph_candidate_weight line 19

Source documentation

Removing the selected squarefree factors leaves exactly the two endpoint complements occurring in the candidate kernel.

theorem arithmetic_graph_candidate_weight {B L T H M u : ℕ} {τ C : ℝ}
    (w : ℕ → ℝ) (v : ℕ → ℕ → ℝ) {e : BlockCandidateIndex M}
    (he : e ∈ blockCandidates B L T H M τ C
      (fun i => coefficientPrimeSet B (u+(i.val+1))))
    (hsq : ¬ BlockSquareHit B M u) :
    arithmeticGraphPairWeight B L τ C w v
      (candidateHigh e) (candidateLow e) (candidateQuotient e) (candidateLag e)
      (u+(e.1.1.val+1))/(B : ℝ) =
    candidateRootWeight B L τ C (fun i => coefficientPrimeSet B (u+(i.val+1)))
      (candidateCutoff w v) e
      (coefficientPrimeSet B (divisorEdgeInverse (candidateHigh e) (candidateLow e)
        (candidateQuotient e) (u+(e.1.1.val+1)))) := by
…

Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.blockCandidates, OAI.JointDickman.coefficientPrimeSet, OAI.JointDickman.BlockSquareHit, OAI.JointDickman.arithmeticGraphPairWeight, OAI.JointDickman.candidateHigh, OAI.JointDickman.candidateLow, OAI.JointDickman.candidateQuotient, OAI.JointDickman.candidateLag, OAI.JointDickman.candidateRootWeight, OAI.JointDickman.candidateCutoff, OAI.JointDickman.divisorEdgeInverse