MultiplicityChernoff.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative lower-tail exponent with a perturbed prefix mean

theorem OAI.JointDickman.multiplicity_chernoff_exponent line 12

Source documentation

The only mean hypothesis is an explicit numerical lower bound. In the application it comes from tilted_prefix_mean_uniform, which uses the published reciprocal-prime Mertens input.

theorem multiplicity_chernoff_exponent {g ℓ ω m τ ε δ r : ℝ}
    (hg : 0 ≤ g) (hℓ : 0 ≤ ℓ) (hτ : 0 ≤ τ) (hε : 0 ≤ ε)
    (hδ : 0 < δ) (hδ1 : δ ≤ 1/2) (hr : 0 ≤ r) (hr1 : r ≤ 1/2)
    (hω : g*r*ℓ ≤ ω) (hm : (g/2-ε)*ℓ ≤ m) :
    let t := -Real.log (2*max δ (1/2-r))
…