PPTTailMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite reciprocal-totient sums for the common factor and the fixed small tail in the PPT comparison argument. A chosen prime list recovers the integer itself, so its reciprocal totient is counted with its full integer multiplicity. No injectivity of the totient function is needed.

lemma OAI.TotientAsymptotic.ppt_prime_pi_mass line 18

theorem OAI.TotientAsymptotic.ppt_fixed_length_tail_mass line 28

Source documentation

A finite family of products of h primes has mass at most the hth power of the available reciprocal shifted-prime mass.

theorem ppt_fixed_length_tail_mass {h : ℕ} (S T : Finset ℕ)
    (p : ℕ → Fin h → ℕ)
    (hprime : ∀ n ∈ S, ∀ i, (p n i).Prime)
    (hmem : ∀ n ∈ S, ∀ i, p n i ∈ T)
    (hreal : ∀ n ∈ S, n = ∏ i, p n i) :
    (∑ n ∈ S, (n.totient : ℝ)⁻¹) ≤
      (∑ q ∈ T, ((q-1 : ℕ) : ℝ)⁻¹)^h := by
…

theorem OAI.TotientAsymptotic.ppt_bounded_length_tail_mass line 69

Source documentation

Summing over all possible factor counts costs only H+1 times the largest of the fixed-length bounds.

theorem ppt_bounded_length_tail_mass (H : ℕ) (T : Finset ℕ)
    (S : ℕ → Finset ℕ) (p : (h : ℕ) → ℕ → Fin h → ℕ)
    (hprime : ∀ h ≤ H, ∀ n ∈ S h, ∀ i, (p h n i).Prime)
    (hmem : ∀ h ≤ H, ∀ n ∈ S h, ∀ i, p h n i ∈ T)
    (hreal : ∀ h ≤ H, ∀ n ∈ S h, n = ∏ i, p h n i) :
    (∑ h ∈ Finset.range (H+1), ∑ n ∈ S h, (n.totient : ℝ)⁻¹) ≤
      (H+1 : ℕ)*
        (max 1 (∑ q ∈ T, ((q-1 : ℕ) : ℝ)⁻¹))^H := by
…