ThreePrimeSingularTail.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.shifted_reciprocal_square_tail line 11
theorem OAI.Problem337.threePrimeOddFactors_tail_abs_sub_one line 31
Source documentation
Every finite tail of the canonical ternary singular series has relative error at most 2 / (N + 1), uniformly in the integer being represented.
```
theorem threePrimeOddFactors_tail_abs_sub_one (u N : ℕ) (P : Finset ℕ)
    (hP : ∀ n ∈ P, N ≤ n) :
    |(∏ n ∈ P, (1 + threePrimeOddPerturbation u n)) - 1| ≤
      2 / ((N : ℝ) + 1) := by
…
```
Mentions: OAI.Problem337.threePrimeOddPerturbation
theorem OAI.Problem337.threePrimeOddFactors_partial_abs_le line 53
Source documentation
Uniform boundedness of the finite odd-prime factors.
```
theorem threePrimeOddFactors_partial_abs_le (u N : ℕ) :
    |∏ n ∈ Finset.range N, (1 + threePrimeOddPerturbation u n)| ≤ 3 := by
…
```
Mentions: OAI.Problem337.threePrimeOddPerturbation
theorem OAI.Problem337.threePrimeOddFactors_tprod_sub_partial line 66
Source documentation
The canonical infinite odd-prime product is uniformly approximated by its first N factors at the explicit rate 6 / (N + 1).
```
theorem threePrimeOddFactors_tprod_sub_partial (u N : ℕ) :
    |(∏' n : ℕ, (1 + threePrimeOddPerturbation u n)) -
      ∏ n ∈ Finset.range N, (1 + threePrimeOddPerturbation u n)| ≤
      6 / ((N : ℝ) + 1) := by
…
```
Mentions: OAI.Problem337.threePrimeOddPerturbation
def OAI.Problem337.threePrimeSingularPartial line 88
Source documentation
The finite canonical singular product, including the factor at two.
```
def threePrimeSingularPartial (u N : ℕ) : ℝ :=
…
```
theorem OAI.Problem337.threePrimeSingularSeries_sub_partial line 93
Source documentation
Uniform quantitative truncation of the actual defined singular series.
```
theorem threePrimeSingularSeries_sub_partial (u N : ℕ) :
    |threePrimeSingularSeries u - threePrimeSingularPartial u N| ≤
      12 / ((N : ℝ) + 1) := by
…
```
Mentions: OAI.Problem337.threePrimeSingularSeries, OAI.Problem337.threePrimeSingularPartial
theorem OAI.Problem337.threePrimeSingularPartial_tendstoUniformly line 106
Source documentation
Uniform convergence in the represented integer: the onset is independent of u, including even inputs where the singular series vanishes.
```
theorem threePrimeSingularPartial_tendstoUniformly :
    TendstoUniformly (fun N u => threePrimeSingularPartial u N)
      threePrimeSingularSeries atTop := by
…
```
Mentions: OAI.Problem337.threePrimeSingularPartial, OAI.Problem337.threePrimeSingularSeries
theorem OAI.Problem337.threePrimeSingularSeries_abs_le_six line 123
Source documentation
A simultaneous absolute bound for all singular series, useful when converting an additive asymptotic error into a relative error.
```
theorem threePrimeSingularSeries_abs_le_six (u : ℕ) :
    |threePrimeSingularSeries u| ≤ 6 := by
…
```
Mentions: OAI.Problem337.threePrimeSingularSeries
theorem OAI.Problem337.threePrimeSingularPartial_sub_tendsto_zero line 135
Source documentation
A cutoff tending to infinity may depend on the represented integer or on any other parameter; uniform truncation still makes the error tend to zero.
```
theorem threePrimeSingularPartial_sub_tendsto_zero {α : Type*} {l : Filter α}
    (u Q : α → ℕ) (hQ : Tendsto Q l atTop) :
    Tendsto (fun x => threePrimeSingularSeries (u x) -
      threePrimeSingularPartial (u x) (Q x)) l (nhds 0) := by
…
```
Mentions: OAI.Problem337.threePrimeSingularSeries, OAI.Problem337.threePrimeSingularPartial
theorem OAI.Problem337.threePrimeSingularPartial_weighted_isLittleO line 147
Source documentation
Truncating the singular series changes any weighted main term by little-o of that same weight. No positivity or nonvanishing of the weight is needed.
```
theorem threePrimeSingularPartial_weighted_isLittleO {α : Type*} {l : Filter α}
    (u Q : α → ℕ) (hQ : Tendsto Q l atTop) (w : α → ℝ) :
    (fun x => (threePrimeSingularSeries (u x) -
      threePrimeSingularPartial (u x) (Q x)) * w x) =o[l] w := by
…
```
Mentions: OAI.Problem337.threePrimeSingularSeries, OAI.Problem337.threePrimeSingularPartial
theorem OAI.Problem337.threePrimeSingularPartial_asymptotic_iff line 159
Source documentation
An asymptotic formula with a growing finite singular product is equivalent to the formula with the canonical infinite series. This supplies the uniform Euler-tail transfer in a major-arc computation without asserting that formula.
```
theorem threePrimeSingularPartial_asymptotic_iff {α : Type*} {l : Filter α}
    (u Q : α → ℕ) (hQ : Tendsto Q l atTop) (a w : α → ℝ) :
    ((fun x => a x - threePrimeSingularSeries (u x) * w x) =o[l] w) ↔
      ((fun x => a x - threePrimeSingularPartial (u x) (Q x) * w x) =o[l] w) := by
…
```
Mentions: OAI.Problem337.threePrimeSingularSeries, OAI.Problem337.threePrimeSingularPartial