RegularValueCount.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The concrete regular-value exception used in the Ford counting bootstrap.

def OAI.TotientAsymptotic.CountingRegular line 15
Source documentation
These are exactly the regularity conditions used in the band count; the preimage conditions hold for every preimage of the value.
```
def CountingRegular (S : ℕ) (X : ℝ) (v : ℕ) : Prop :=
…
```
def OAI.TotientAsymptotic.nonNormalValues line 20
theorem OAI.TotientAsymptotic.regular_value_exception_count line 24

theorem OAI.TotientAsymptotic.regular_value_envelope_bound line 89

Source documentation

The complete regular-value exception bound, with every arithmetic input proved and the remaining scale parameters explicit.

theorem regular_value_envelope_bound : ∃ A D C E : ℝ,
    0 < A ∧ 0 < D ∧ 0 < C ∧ 0 < E ∧
    ∀ (S X N J : ℕ),2 < (S:ℝ) → 0 ≤ B S → 16 ≤ X →
    Real.exp (Real.exp 1) ≤ X → 4 ≤ N → (N:ℝ)^2 ≤ X →
    (X:ℝ)^(1/4:ℝ) ≤ N → 1 ≤ J → (X:ℝ) ≤ (2:ℝ)^J →
    ∀ Q : Finset ℕ,(∀ v ∈ Q,IsTotient v ∧ v ≤ X ∧ ¬CountingRegular S X v) →
    (Q.card:ℝ) ≤ A*X*(Real.log X)^(-5/4:ℝ)+(2*X+D*X*B X)/(S+1:ℕ)+
      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:ℝ)+
      (E*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.A, OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.IsTotient, OAI.TotientAsymptotic.CountingRegular, OAI.TotientAsymptotic.dyadicTotientEnvelope