OAI/NumberTheory/JointDickman/Counting/BlockCandidates.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The finite candidate representations determined by endpoint types

  1. def OAI.JointDickman.endpointSplits line 13
  2. theorem OAI.JointDickman.mem_endpointSplits line 16
  3. theorem OAI.JointDickman.endpointSplits_card line 22
  4. abbrev OAI.JointDickman.BlockCandidateIndex line 39
  5. def OAI.JointDickman.candidateLow line 43

    Source documentation

    Lower and upper endpoint subsets; the coefficient c is determined by these two subset products and the positive lag.

    noncomputable def candidateLow {M : ℕ} (e : BlockCandidateIndex M) : ℕ := ∏ p ∈ e.2.1, p

    Mentions: OAI.JointDickman.BlockCandidateIndex

  6. def OAI.JointDickman.candidateHigh line 44
  7. def OAI.JointDickman.candidateLag line 45
  8. def OAI.JointDickman.candidateQuotient line 46
  9. def OAI.JointDickman.blockCandidatePool line 50
  10. def OAI.JointDickman.BlockCandidateAdmissible line 56
  11. def OAI.JointDickman.blockCandidates line 72
  12. theorem OAI.JointDickman.blockCandidatePool_card line 76
  13. theorem OAI.JointDickman.blockCandidates_card line 96