PrimeBox.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Unit-box prime sums. The conditional input is the one-dimensional Mertens estimate displayed in the proof of Ford, The distribution of totients, arXiv:1104.3264v2 (2013), Lemma 3.1, p. 11: the reciprocal-shift sum over exp(exp(m-1)) ≤ p < exp(exp(m)) equals 1 + O(exp(-m)).

def OAI.TotientAsymptotic.unitPrimeBox line 17
def OAI.TotientAsymptotic.unitPrimeWeight line 22
def OAI.TotientAsymptotic.FordUnitPrimeBoxInput line 24
lemma OAI.TotientAsymptotic.unitPrimeWeight_nonneg line 28
lemma OAI.TotientAsymptotic.abs_prod_sub_one_le line 35
lemma OAI.TotientAsymptotic.abs_prod_sub_one_le_exp line 61
theorem OAI.TotientAsymptotic.prime_unit_box_error line 76
Source documentation
The relative error in a multidimensional unit box depends on the sum of the one-dimensional errors, rather than directly on the number of coordinates.
```
theorem prime_unit_box_error (hford : FordUnitPrimeBoxInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ {ι : Type*} (I : Finset ι) (m : ι → ℕ),
      (∀ i ∈ I, 1 ≤ m i) →
      |(∏ i ∈ I, unitPrimeWeight (m i))-1| ≤
        Real.exp (C*∑ i ∈ I, Real.exp (-(m i : ℝ)))-1 := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.unitPrimeWeight