OAI/NumberTheory/TwoPoint/Bounds/LabeledPrimeWords.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Identifying squarefree-label polynomials with numerical signed words.

  1. structure OAI.TwoPointCorrelations.LabeledPrimeWord line 13
  2. def OAI.TwoPointCorrelations.LabeledPrimeWord.Realizes line 21
  3. def OAI.TwoPointCorrelations.LabeledPrimeWord.monomial line 24
  4. lemma OAI.TwoPointCorrelations.LabeledPrimeWord.monomial_eval line 29
  5. lemma OAI.TwoPointCorrelations.LabeledPrimeWord.label_iff_occurrence line 37
  6. def OAI.TwoPointCorrelations.LabeledPrimeWord.intervalRelation line 52

    Source documentation

    A genuine interval relation; omitted steps have empty supports as well as zero coefficients. This matters for the later-variable exclusion.

    def intervalRelation (w : LabeledPrimeWord ι) (h a b : ℕ) (i : Fin w.word.length) : PrimeMonomial ι :=
…

    Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord, OAI.TwoPointCorrelations.PrimeMonomial

  7. lemma OAI.TwoPointCorrelations.LabeledPrimeWord.intervalRelation_support line 55
  8. lemma OAI.TwoPointCorrelations.sum_fin_interval line 69
  9. lemma OAI.TwoPointCorrelations.LabeledPrimeWord.intervalRelation_eval line 83
  10. lemma OAI.TwoPointCorrelations.LabeledPrimeWord.intervalRelation_contribution line 98
  11. def OAI.TwoPointCorrelations.LabeledPrimeWord.fromPrimeSet line 128

    Source documentation

    A canonical finite label model, using the actual prime factors of each whole tuple inside one finite prime pool.

    def fromPrimeSet (word : List SignedStep) (P : Finset ℕ) : LabeledPrimeWord P where
…

    Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.LabeledPrimeWord

  12. lemma OAI.TwoPointCorrelations.LabeledPrimeWord.fromPrimeSet_realizes line 132