IntervalChernoff.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exponential deviation estimates for reciprocal cofactor mass.

lemma OAI.TotientAsymptotic.exp_small_tilt line 10

theorem OAI.TotientAsymptotic.interval_omega_chernoff line 23

Source documentation

A single estimate handles the upper and lower tails by choosing the sign of t. The mass uses every prime factor with multiplicity.

theorem interval_omega_chernoff : ∃ C : ℝ, 0<C ∧
    ∀ N : ℕ, 2≤N → ∀ U T : ℝ, 2≤U → U≤T → T≤N →
    ∀ t h : ℝ, |t|≤1/4 → ∀ Q : Finset ℕ,
    (∀ n ∈ Q,0<n ∧ n≤N ∧ |t| *h≤t*((omegaIn n U T:ℝ)-(B T-B U))) →
    (∑ n ∈ Q,(n:ℝ)⁻¹) ≤ C*Real.log N*
      Real.exp (t^2*(B T-B U)-|t| *h) := by
…

Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.omegaIn, OAI.TotientAsymptotic.B