DivisorPointwiseUniform.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.divisorPointwiseError line 10
Source documentation
An explicit uniform error coefficient for the pointwise truncated-divisor estimate.
```
def divisorPointwiseError (E S : ℝ) : ℝ :=
…
```
theorem OAI.Problem337.divisorPointwiseError_tendsto line 14

theorem OAI.Problem337.truncatedDivisorCount_pointwise_error_bound line 31

Source documentation

Explicit estimate uniform over the admissible logarithmic size interval.

theorem truncatedDivisorCount_pointwise_error_bound (E S X : ℝ) {n : ℕ}
    (hE : 1 ≤ E) (hS : 1 < S) (hES : 1 + E / Real.log 2 ≤ S)
    (hn : n ≠ 0) (hX : 1 < X)
    (hlo : S / (2 * Real.log S) ≤ Real.log X)
    (hhi : Real.log X ≤ E * S) (hnhi : Real.log (n : ℝ) ≤ E * S) :
    Real.log (truncatedDivisorCount X n : ℝ) ≤ divisorPointwiseError E S * Real.log X := by
…

Mentions: OAI.Problem337.truncatedDivisorCount, OAI.Problem337.divisorPointwiseError

theorem OAI.Problem337.truncatedDivisorCount_uniform_subpower line 94

Source documentation

Uniform subpower growth of truncated divisor moments over the full size interval.

theorem truncatedDivisorCount_uniform_subpower (E r ε : ℝ) (hE : 1 ≤ E)
    (hr : 0 ≤ r) (hε : 0 < ε) :
    ∃ S0 : ℝ, ∀ S : ℝ, S0 ≤ S → ∀ X : ℝ, ∀ n : ℕ,
      n ≠ 0 → 1 < X → S / (2 * Real.log S) ≤ Real.log X →
      Real.log X ≤ E * S → Real.log (n : ℝ) ≤ E * S →
      (truncatedDivisorCount X n : ℝ) ^ r ≤ Real.exp (ε * Real.log X) := by
…

Mentions: OAI.Problem337.truncatedDivisorCount

theorem OAI.Problem337.truncatedDivisorCount_shifted_uniform_subpower line 123

Source documentation

The uniform pointwise estimate in the shifted-interval range of the moment lemma.

theorem truncatedDivisorCount_shifted_uniform_subpower (D r ε : ℝ) (hD : 1 ≤ D)
    (hr : 0 ≤ r) (hε : 0 < ε) :
    ∃ S0 : ℝ, ∀ S : ℝ, S0 ≤ S → ∀ X Y : ℝ, ∀ N h : ℕ,
      1 ≤ X → S / (2 * Real.log S) ≤ Real.log X →
      Real.log X ≤ D * S → (N : ℝ) ≤ Real.exp (D * S) →
      1 ≤ h → (h : ℝ) ≤ Y → Y ≤ X →
      (truncatedDivisorCount X (N + h) : ℝ) ^ r ≤ Real.exp (ε * Real.log X) := by
…

Mentions: OAI.Problem337.D, OAI.Problem337.truncatedDivisorCount