SmallPrimeValueCount.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The small-prime half of the exceptional-value count in Ford Lemma 2.8. The envelope counts residual totient values, independently of fiber sizes.

lemma OAI.TotientAsymptotic.small_divisor_value_bound line 14

theorem OAI.TotientAsymptotic.small_prime_value_count line 44

Source documentation

Prime divisors up to the square-root scale, with no choice of preimage counted more than once.

theorem small_prime_value_count {x : ℝ} {J : ℕ} (hx : 16 ≤ x)
    (hJ : x ≤ (2:ℝ)^J) (P Q : Finset ℕ)
    (hP : ∀ p ∈ P,p.Prime ∧ (p:ℝ)^2 ≤ x)
    (hQ : ∀ v ∈ Q,∃ n p : ℕ,0 < n ∧ n.totient=v ∧ p.Prime ∧ p ∣ n ∧
      (v:ℝ) ≤ x ∧ p ∈ P) :
    (Q.card:ℝ) ≤ (16*dyadicTotientEnvelope J*x/Real.log x)*
      ∑ p ∈ P,((p-1:ℕ):ℝ)⁻¹ := by
…

Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.dyadicTotientEnvelope

theorem OAI.TotientAsymptotic.small_non_normal_value_count line 65

Source documentation

The exceptional-value bound for small prime factors.

theorem small_non_normal_value_count : ∃ C : ℝ,0 < C ∧
    ∀ (S x : ℝ) (N J : ℕ),2 < S → 0 ≤ B S → 4 ≤ N → 16 ≤ x →
    (N:ℝ)^2 ≤ x → x ≤ (2:ℝ)^J → ∀ Q : Finset ℕ,
    (∀ v ∈ Q,∃ n p : ℕ,0 < n ∧ n.totient=v ∧ p.Prime ∧ p ∣ n ∧
      (v:ℝ) ≤ x ∧ p ≤ N ∧ ¬IsNormalPrime S p) →
    (Q.card:ℝ) ≤ C*dyadicTotientEnvelope J*x/Real.log x*
      (B ((2:ℝ)^(Nat.clog 2 N)))^5*(1+Real.log (Nat.clog 2 N))*
        (Real.log S)^(-1/6:ℝ) := by
…

Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.dyadicTotientEnvelope