ThreePrimeEulerTail.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.ThreePrimeEulerTail.reciprocal_square_tail line 11
Source documentation
A reciprocal-square tail is bounded by a telescoping reciprocal tail. The statement is for arbitrary finite sets, hence also for sets of primes.
```
theorem reciprocal_square_tail (P : Finset ℕ) (N : ℕ) (hN : 2 ≤ N)
    (hP : ∀ p ∈ P, N < p) :
    (∑ p ∈ P, 1 / ((p : ℝ) - 1) ^ 2) ≤ 1 / ((N : ℝ) - 1) := by
…
```

theorem OAI.Problem337.ThreePrimeEulerTail.product_tail_abs_sub_one line 63

Source documentation

Uniform finite Euler-tail error from the standard local-factor defect bound.

theorem product_tail_abs_sub_one (f : ℕ → ℝ) (P : Finset ℕ)
    (N : ℕ) (hN : 2 ≤ N) (hP : ∀ p ∈ P, N < p)
    (hf : ∀ p ∈ P, |f p - 1| ≤ 1 / ((p : ℝ) - 1) ^ 2) :
    |(∏ p ∈ P, f p) - 1| ≤ 2 / ((N : ℝ) - 1) := by
…

theorem OAI.Problem337.ThreePrimeEulerTail.summable_abs_sub_one line 85
Source documentation
The local-factor defect majorant gives absolute summability without imposing any condition on the finitely many initial factors.
```
theorem summable_abs_sub_one (f : ℕ → ℝ)
    (hf : ∀ p : ℕ, 3 ≤ p → |f p - 1| ≤ 1 / ((p : ℝ) - 1) ^ 2) :
    Summable (fun p => |f p - 1|) := by
…
```
theorem OAI.Problem337.ThreePrimeEulerTail.multipliable line 100
Source documentation
Absolute summability of the local defects defines a genuine Euler product.
```
theorem multipliable (f : ℕ → ℝ)
    (hf : ∀ p : ℕ, 3 ≤ p → |f p - 1| ≤ 1 / ((p : ℝ) - 1) ^ 2) :
    Multipliable f := by
…
```

theorem OAI.Problem337.ThreePrimeEulerTail.tprod_sub_partial_abs_le line 110

Source documentation

A partial Euler product approximates its infinite product with an explicit relative error. Only the universal local defect estimate is needed.

theorem tprod_sub_partial_abs_le (f : ℕ → ℝ)
    (hf : ∀ p : ℕ, 3 ≤ p → |f p - 1| ≤ 1 / ((p : ℝ) - 1) ^ 2)
    (N : ℕ) (hN : 2 ≤ N) :
    |(∏' p, f p) - ∏ p ∈ Finset.range (N + 1), f p| ≤
      |∏ p ∈ Finset.range (N + 1), f p| * (2 / ((N : ℝ) - 1)) := by
…

theorem OAI.Problem337.ThreePrimeEulerTail.partial_abs_le line 137

Source documentation

All partial products are bounded by three times their first three factors. This estimate is uniform in any external parameter of the local factors.

theorem partial_abs_le (f : ℕ → ℝ)
    (hf : ∀ p : ℕ, 3 ≤ p → |f p - 1| ≤ 1 / ((p : ℝ) - 1) ^ 2)
    (N : ℕ) (hN : 2 ≤ N) :
    |∏ p ∈ Finset.range (N + 1), f p| ≤
      3 * |∏ p ∈ Finset.range 3, f p| := by
…

theorem OAI.Problem337.ThreePrimeEulerTail.tprod_sub_partial_abs_le_uniform line 156

Source documentation

Uniform O(1/N) truncation error, stated with a bound for the only three uncontrolled initial local factors.

theorem tprod_sub_partial_abs_le_uniform (f : ℕ → ℝ)
    (hf : ∀ p : ℕ, 3 ≤ p → |f p - 1| ≤ 1 / ((p : ℝ) - 1) ^ 2)
    (B : ℝ) (hB : |∏ p ∈ Finset.range 3, f p| ≤ B)
    (N : ℕ) (hN : 2 ≤ N) :
    |(∏' p, f p) - ∏ p ∈ Finset.range (N + 1), f p| ≤
      6 * B / ((N : ℝ) - 1) := by
…