OAI/NumberTheory/TwoPoint/Walks/TuplePrimeArithmetic.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Disjoint prime pools give the actual tuple factorization and unique tuple labels.

  1. lemma OAI.TwoPointCorrelations.selectedPrimeValues_injective line 13
  2. lemma OAI.TwoPointCorrelations.columnTuple_primeFactors line 23
  3. lemma OAI.TwoPointCorrelations.columnTuple_primeFactors_card line 32
  4. lemma OAI.TwoPointCorrelations.columnTuple_squarefree line 41
  5. theorem OAI.TwoPointCorrelations.primeTuple_injective line 58

    Source documentation

    The numerical whole tuple determines its column choices, as used by the nonbacktracking matrix's actual copy labels.

    theorem primeTuple_injective {J : ℕ} {P : Fin J → Finset ℕ}
    (hprime : ∀ j, ∀ p ∈ P j, p.Prime)
    (hdisjoint : ∀ j l, l ≠ j → Disjoint (P j) (P l)) :
    Function.Injective (fun x : (j : Fin J) → P j => ∏ j, (x j).val) := by
…