PPTTotientSquare.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The large-square-in-a-totient branch of the PPT pruning argument. Euler's product formula reduces it to a square in the integer, a square in one prime predecessor, or a common factor of two distinct prime predecessors. Elementary reciprocal divisor bounds suffice when the cutoff is a sufficiently large fixed power of the logarithm.

theorem OAI.TotientAsymptotic.ppt_totient_square_cases line 19
def OAI.TotientAsymptotic.pptDivisorMultiples line 46
lemma OAI.TotientAsymptotic.ppt_multiples_mem line 49
lemma OAI.TotientAsymptotic.ppt_multiples_card line 53
lemma OAI.TotientAsymptotic.ppt_shift_prime_mem line 59
lemma OAI.TotientAsymptotic.ppt_shift_prime_reciprocal line 65
theorem OAI.TotientAsymptotic.ppt_fixed_totient_square_count line 76
Source documentation
A fixed prime-square divisor of a totient is rare among all integers, without any restriction on their total number of prime factors.
```
theorem ppt_fixed_totient_square_count {N p : ℕ} (hp : p.Prime)
    (Q : Finset ℕ) (hQ : ∀ n ∈ Q, 0 < n ∧ n ≤ N ∧ p^2 ∣ n.totient) :
    (Q.card : ℝ) ≤ (N : ℝ)*(1+(1+Real.log N)+(1+Real.log N)^2)/(p : ℝ)^2 := by
…
```
Mentions: OAI.TotientAsymptotic.N

theorem OAI.TotientAsymptotic.ppt_large_totient_square_count line 160

Source documentation

Summing over the large square divisor uses the already proved inverse square tail; the resulting cutoff may be any positive integer.

theorem ppt_large_totient_square_count {N K : ℕ} (hN : 1 ≤ N) (hK : 1 ≤ K)
    (Q : Finset ℕ)
    (hQ : ∀ n ∈ Q, 0 < n ∧ n ≤ N ∧ ∃ p : ℕ, p.Prime ∧ K < p ∧ p^2 ∣ n.totient) :
    (Q.card : ℝ) ≤ 6*(N : ℝ)*(1+Real.log N)^2/(K : ℝ) := by
…

Mentions: OAI.TotientAsymptotic.N