ThetaLogError.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

An integrable logarithmic error bound obtained from the stated exponential prime-number error. It also pays exactly for finite exceptional prime sets.

lemma OAI.TwoPointCorrelations.exp_neg_sqrt_log_le line 13
Also declared: OAI/NumberTheory/TwoPointCorrelations/ThetaLogError.lean:13 (same declaration text).
lemma OAI.TwoPointCorrelations.log_sq_le_two_mul line 36
Also declared: OAI/NumberTheory/TwoPointCorrelations/ThetaLogError.lean:36 (same declaration text).
theorem OAI.TwoPointCorrelations.ModFiveThetaInput.log_error line 44
Source documentation
A single constant controls the logarithmic PNT error for both residue selections and every real endpoint at least two.
Also declared: OAI/NumberTheory/TwoPointCorrelations/ThetaLogError.lean:44 (same declaration text).
```
theorem ModFiveThetaInput.log_error (hP : ModFiveThetaInput) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ (one : Bool) (x : ℝ), 2 ≤ x →
      |modFiveTheta one x - modFiveDensity one * x| ≤ K * x / Real.log x ^ 2 := by
…
```
Mentions: OAI.TwoPointCorrelations.ModFiveThetaInput, OAI.TwoPointCorrelations.modFiveTheta, OAI.TwoPointCorrelations.modFiveDensity
theorem OAI.TwoPointCorrelations.ModFiveThetaInput.deleted_log_error line 55
Also declared: OAI/NumberTheory/TwoPointCorrelations/ThetaLogError.lean:55 (same declaration text).