OAI/NumberTheory/TwoPointCorrelations/RetainedDivisorMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The literal finite retained-divisor set and its Euler-product mass. Distinct prime subsets produce distinct integers, so the divisor sum does not contain hidden multiplicities.

  1. def OAI.TwoPointCorrelations.retainedPrimeDivisors line 17

    Also declared: OAI/NumberTheory/TwoPoint/Walks/RetainedDivisorMass.lean:17 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.primeSubset_product_injective line 20

    Also declared: OAI/NumberTheory/TwoPoint/Walks/RetainedDivisorMass.lean:20 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.retainedPrimeDivisor_pos line 30

    Also declared: OAI/NumberTheory/TwoPoint/Walks/RetainedDivisorMass.lean:30 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.retainedPrimeDivisor_factors line 35

    Also declared: OAI/NumberTheory/TwoPoint/Walks/RetainedDivisorMass.lean:35 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.retainedPrimeDivisor_card_factors line 42

    Also declared: OAI/NumberTheory/TwoPoint/Walks/RetainedDivisorMass.lean:42 (same declaration text).

  6. theorem OAI.TwoPointCorrelations.retainedPrimeDivisors_weighted_mass line 46

    Also declared: OAI/NumberTheory/TwoPoint/Walks/RetainedDivisorMass.lean:46 (same declaration text).