OAI/NumberTheory/JointDickman/Amplification/CandidateRootGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness of a representation at a fixed pair of endpoints

  1. theorem OAI.JointDickman.mem_blockCandidatePool line 11
  2. theorem OAI.JointDickman.mem_blockCandidates line 29
  3. def OAI.JointDickman.blockCandidateRoot line 37
  4. theorem OAI.JointDickman.blockCandidate_same_pair_root_unique line 42

    Source documentation

    On a fixed unordered pair the rational root specifies both endpoint subset products, and hence the unique candidate representation.

    theorem blockCandidate_same_pair_root_unique {B L T H M : ℕ} {τ C : ℝ}
    {S : Fin M → Finset ℕ} (hS : ∀ i, S i ⊆ auxiliaryPrimes B)
    {e f : BlockCandidateIndex M}
    (he : e ∈ blockCandidates B L T H M τ C S)
    (hf : f ∈ blockCandidates B L T H M τ C S)
    (hpair : e.1 = f.1) (hroot : blockCandidateRoot e = blockCandidateRoot f) : e = f := by
…

    Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.blockCandidates, OAI.JointDickman.blockCandidateRoot