OAI/NumberTheory/TotientAsymptotic/OrderedFactorizations.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Concrete finite encodings for ordered multiplicative factorizations.

  1. def OAI.TotientAsymptotic.multiplyFactor line 12
  2. lemma OAI.TotientAsymptotic.prod_multiplyFactor line 15
  3. def OAI.TotientAsymptotic.factorAllocations line 22
  4. lemma OAI.TotientAsymptotic.factorAllocations_card_le line 27
  5. lemma OAI.TotientAsymptotic.mem_factorAllocations line 38
  6. theorem OAI.TotientAsymptotic.paired_factorizations_card_le line 67

    Source documentation

    Independent left and right allocations give the collision multiplicity.

    theorem paired_factorizations_card_le (k n : ℕ) (hn : 0 < n)
    (Q : Finset ((Fin k → ℕ) × (Fin k → ℕ)))
    (hQ : ∀ f ∈ Q,(∏ j,f.1 j)=n ∧ (∏ j,f.2 j)=n) :
    Q.card ≤ k^(2*n.primeFactorsList.length) := by
…