ThreePrimeSingularSeries.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.threePrimeOddPerturbation line 12
Source documentation
The odd-prime local perturbation in the ternary Goldbach singular series. Index n corresponds to the integer n + 3; nonprimes contribute zero.
```
def threePrimeOddPerturbation (u n : ℕ) : ℝ :=
…
```
def OAI.Problem337.threePrimeSingularSeries line 19
Source documentation
The local factor at two, with all the odd-prime factors following it.
```
def threePrimeSingularSeries (u : ℕ) : ℝ :=
…
```
lemma OAI.Problem337.threePrimeOddPerturbation_norm_le line 23
lemma OAI.Problem337.threePrimeOddPerturbation_summable line 36
lemma OAI.Problem337.threePrimeOddFactors_multipliable line 43
lemma OAI.Problem337.prod_one_sub_reciprocal_square line 49
Source documentation
The telescoping product over all integers is a lower bound for the product of the negative local factors over any subset of odd primes.
```
lemma prod_one_sub_reciprocal_square (N : ℕ) :
    (∏ n ∈ Finset.range N, (1 - 1 / ((n : ℝ) + 2) ^ 2)) =
      ((N : ℝ) + 2) / (2 * ((N : ℝ) + 1)) := by
…
```
lemma OAI.Problem337.one_sub_reciprocal_square_nonneg line 62
lemma OAI.Problem337.threePrimeOddFactor_lower line 69
lemma OAI.Problem337.threePrimeOddFactors_prod_lower line 76
lemma OAI.Problem337.threePrimeOddFactors_tprod_lower line 88
theorem OAI.Problem337.threePrimeSingularSeries_one_le line 95
Source documentation
Uniform positivity does not require a prime number theorem: the all-integer comparison product gives the explicit lower bound one for every odd input.
```
theorem threePrimeSingularSeries_one_le {u : ℕ} (hu : Odd u) :
    1 ≤ threePrimeSingularSeries u := by
…
```
Mentions: OAI.Problem337.threePrimeSingularSeries
theorem OAI.Problem337.quantitativeThreePrimeLowerBound_of_singular_error line 104
Source documentation
A uniform asymptotic error estimate for ordered prime triples suffices for the precise quantitative number-theoretic interface used by the supply proof. The asymptotic estimate remains a hypothesis; no Vinogradov theorem is asserted.
```
theorem quantitativeThreePrimeLowerBound_of_singular_error
    (A : ℝ) (hA : 0 < A)
    (herror : ∀ ε : ℝ, 0 < ε → ∀ᶠ u : ℕ in atTop, Odd u →
      |((supplyPrimeTriples u).card : ℝ) - A * threePrimeSingularSeries u *
        ((u : ℝ) ^ 2 / Real.log (u : ℝ) ^ 3)| ≤
      ε * ((u : ℝ) ^ 2 / Real.log (u : ℝ) ^ 3)) :
    QuantitativeThreePrimeLowerBound := by
…
```
Mentions: OAI.Problem337.supplyPrimeTriples, OAI.Problem337.threePrimeSingularSeries, OAI.Problem337.QuantitativeThreePrimeLowerBound