DivisorLocalFactor.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.DivisorMoment.summable_shifted_pow_geometric line 8
Source documentation
Polynomially weighted geometric series, with the indexing used by the nonconstant terms of an Euler factor.
```
theorem summable_shifted_pow_geometric (r : ℕ) {ρ : ℝ}
    (hρ0 : 0 < ρ) (hρ1 : ρ < 1) :
    Summable (fun j : ℕ => ((j : ℝ) + 2) ^ r * ρ ^ j) := by
…
```

theorem OAI.Problem337.DivisorMoment.local_factor_linear_bound line 22

Source documentation

All nonconstant coefficients of the Euler factor have a uniform linear majorant on any fixed compact subinterval of the geometric convergence disk.

theorem local_factor_linear_bound (r : ℕ) {ρ : ℝ}
    (hρ0 : 0 < ρ) (hρ1 : ρ < 1) :
    ∃ C : ℝ, 0 < C ∧ ∀ x : ℝ, 0 ≤ x → x ≤ ρ →
      Summable (fun j : ℕ => ((j : ℝ) + 2) ^ r * x ^ (j + 1)) ∧
      (∑' j : ℕ, ((j : ℝ) + 2) ^ r * x ^ (j + 1)) ≤ C * x ∧
      Real.log (1 + ∑' j : ℕ, ((j : ℝ) + 2) ^ r * x ^ (j + 1)) ≤ C * x := by
…

theorem OAI.Problem337.DivisorMoment.local_factor_real_moment_bound line 57

Source documentation

Real moments are reduced to a larger integral moment, uniformly in x.

theorem local_factor_real_moment_bound (r : ℝ) {ρ : ℝ}
    (hρ0 : 0 < ρ) (hρ1 : ρ < 1) :
    ∃ C : ℝ, 0 < C ∧ ∀ x : ℝ, 0 ≤ x → x ≤ ρ →
      Summable (fun j : ℕ => ((j : ℝ) + 2) ^ r * x ^ (j + 1)) ∧
      (∑' j : ℕ, ((j : ℝ) + 2) ^ r * x ^ (j + 1)) ≤ C * x ∧
      Real.log (1 + ∑' j : ℕ, ((j : ℝ) + 2) ^ r * x ^ (j + 1)) ≤ C * x := by
…

theorem OAI.Problem337.DivisorMoment.divisor_local_factor_bound line 87

Source documentation

Uniform local Euler-factor bound. Primality is unnecessary; p≥2 is enough. The range σ≤1 can also be omitted from this local estimate.

theorem divisor_local_factor_bound (r : ℝ) :
    ∃ C : ℝ, 0 < C ∧ ∀ p σ : ℝ, 2 ≤ p → (3 / 4 : ℝ) ≤ σ →
      Summable (fun j : ℕ => ((j : ℝ) + 2) ^ r * (p ^ (-σ)) ^ (j + 1)) ∧
      Real.log (1 + ∑' j : ℕ, ((j : ℝ) + 2) ^ r * (p ^ (-σ)) ^ (j + 1)) ≤
        C * p ^ (-σ) := by
…

theorem OAI.Problem337.DivisorMoment.full_local_factor_bounds line 110

Source documentation

Convert the shifted nonconstant series to the full Euler factor and all its finite partial sums.

theorem full_local_factor_bounds {r x B : ℝ} (hx : 0 ≤ x)
    (hs : Summable (fun j : ℕ => ((j : ℝ) + 2) ^ r * x ^ (j + 1)))
    (hlog : Real.log (1 + ∑' j : ℕ, ((j : ℝ) + 2) ^ r * x ^ (j + 1)) ≤ B) :
    Summable (fun j : ℕ => ((j : ℝ) + 1) ^ r * x ^ j) ∧
    Real.log (∑' j : ℕ, ((j : ℝ) + 1) ^ r * x ^ j) ≤ B ∧
    ∀ L : ℕ, Real.log (∑ j ∈ Finset.range (L + 1),
      ((j : ℝ) + 1) ^ r * x ^ j) ≤ B := by
…

theorem OAI.Problem337.DivisorMoment.divisor_full_local_factor_bound line 138

Source documentation

Full and finite Euler factors, with a uniform constant for every real moment and every σ≥3/4. This is convenient for both finite and infinite Euler-product arguments.

theorem divisor_full_local_factor_bound (r : ℝ) :
    ∃ C : ℝ, 0 < C ∧ ∀ p σ : ℝ, 2 ≤ p → (3 / 4 : ℝ) ≤ σ →
      Summable (fun j : ℕ => ((j : ℝ) + 1) ^ r * (p ^ (-σ)) ^ j) ∧
      Real.log (∑' j : ℕ, ((j : ℝ) + 1) ^ r * (p ^ (-σ)) ^ j) ≤ C * p ^ (-σ) ∧
      ∀ L : ℕ, Real.log (∑ j ∈ Finset.range (L + 1),
        ((j : ℝ) + 1) ^ r * (p ^ (-σ)) ^ j) ≤ C * p ^ (-σ) := by
…