SquarePreimageCount.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Large-square exceptions may occur in any preimage of a totient value.

lemma OAI.TotientAsymptotic.large_square_preimage_count line 11

theorem OAI.TotientAsymptotic.square_preimage_exception_count line 31

Source documentation

Uniformly counts values with a repeated large factor in some preimage. The log-log preimage bound applies to every preimage, so no least-preimage choice or fiber bound is involved.

theorem square_preimage_exception_count : ∃ C : ℝ,0 < C ∧
    ∀ x : ℝ,Real.exp (Real.exp 1) ≤ x → ∀ K : ℕ,∀ Q : Finset ℕ,
    (∀ v ∈ Q,∃ n : ℕ,0 < n ∧ n.totient=v ∧ (v:ℝ) ≤ x ∧
      ∃ d : ℕ,K < d ∧ d^2 ∣ n) →
    (Q.card:ℝ) ≤ C*x*B x/(K+1:ℕ) := by
…

Mentions: OAI.TotientAsymptotic.B