OAI/NumberTheory/TwoPointCorrelations/CenterBandExpansion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact expansion of the center-band factors. Each nonempty choice of constant factors leaves an ordinary divisibility condition for the retained prime product, and carries precisely one reciprocal removed-prime product.

  1. def OAI.TwoPointCorrelations.natDivisibilityIndicator line 15

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/CenterBandExpansion.lean:15 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.primeProduct_dvd_iff line 17

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/CenterBandExpansion.lean:17 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.natDivisibilityIndicator_product line 29

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/CenterBandExpansion.lean:29 (same declaration text).

  4. theorem OAI.TwoPointCorrelations.centerBand_expansion line 46

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/CenterBandExpansion.lean:46 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.primeSubset_product_one_lt line 60

    Source documentation

    A nonempty removed-prime set contributes a nontrivial factor w>1.

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/CenterBandExpansion.lean:60 (same declaration text).

    lemma primeSubset_product_one_lt (W : Finset ℕ) (hW : ∀ p ∈ W, Nat.Prime p)
    (hne : W.Nonempty) : 1 < ∏ p ∈ W, p := by
…
  6. lemma OAI.TwoPointCorrelations.primeSubset_factorization line 67

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/CenterBandExpansion.lean:67 (same declaration text).