ExceptionalValueCount.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The complete non-normal-prime contribution to Ford's nice-value exception. All fibers are handled by finite value covers, without multiplicity weights.

lemma OAI.TotientAsymptotic.totient_div_prime_le line 13

theorem OAI.TotientAsymptotic.non_normal_value_count_split line 25

Source documentation

A finite, uniform form of the non-normal-prime part of Ford Lemma 2.8. The two numeric inequalities select any cutoff between the fourth-root and square-root scales.

theorem non_normal_value_count_split : ∃ C D : ℝ,0 < C ∧ 0 < D ∧
    ∀ (S x : ℝ) (N J : ℕ),2 < S → 0 ≤ B S → 4 ≤ N → 16 ≤ x →
    (N:ℝ)^2 ≤ x → x^(1/4:ℝ) ≤ N → 1 ≤ J → x ≤ (2:ℝ)^J →
    ∀ Q : Finset ℕ,
    (∀ v ∈ Q,∃ n p : ℕ,0 < n ∧ n.totient=v ∧ p.Prime ∧ p ∣ n ∧
      (v:ℝ) ≤ x ∧ ¬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:ℝ) +
      (D*x/Real.log x*(B (2*x))^5*(Real.log S)^(-1/6:ℝ))*
        (1+4*dyadicTotientEnvelope J*(1+Real.log J)) := by
…

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