LargeClassUniform.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.DivisorClasses.LargeClass.inLargePrefixClass line 15
Source documentation
The canonical sorted-prefix large class satisfies the hypotheses of the weighted large-prefix estimate.
```
theorem DivisorClasses.LargeClass.inLargePrefixClass {n : ℕ} {v Y : ℝ}
    (h : DivisorClasses.LargeClass n v Y) :
    InLargePrefixClass (Real.sqrt Y) (v ^ (15 / 16 : ℝ)) n := by
…
```
Mentions: OAI.Problem337.v, OAI.Problem337.DivisorClasses.LargeClass, OAI.Problem337.InLargePrefixClass

theorem OAI.Problem337.shifted_log_le_enlarged_scale line 25

Source documentation

Normalizing the size of the translated integer costs only one extra S in its logarithmic bound.

theorem shifted_log_le_enlarged_scale (D S X Y : ℝ) (N h : ℕ)
    (hSlog : Real.log 2 ≤ S) (hX : 0 < X)
    (hhi : Real.log X ≤ D * S) (hN : (N : ℝ) ≤ Real.exp (D * S))
    (hh : 1 ≤ h) (hhY : (h : ℝ) ≤ Y) (hYX : Y ≤ X) :
    Real.log ((N + h : ℕ) : ℝ) ≤ (D + 1) * S := by
…

Mentions: OAI.Problem337.D

theorem OAI.Problem337.eventually_large_class_moment_bound line 50

Source documentation

The complete eventual large-class estimate in the uniform moment range. All prefix, harmonic, and translated-size hypotheses are discharged; only the manuscript's size window remains.

theorem eventually_large_class_moment_bound (D r : ℝ) (_hD : 1 ≤ D) (hr : 0 ≤ r) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ S : ℝ in atTop, ∀ X Y : ℝ, ∀ N : ℕ,
      S / (2 * Real.log S) ≤ Real.log X → Real.log X ≤ D * S →
      Real.sqrt X ≤ Y → Y ≤ X → (N : ℝ) ≤ Real.exp (D * S) →
      (∑ h ∈ (Finset.Icc 1 ⌊Y⌋₊).filter
        (fun h => DivisorClasses.LargeClass (N + h) (Real.log X) Y),
        (truncatedDivisorCount X (N + h) : ℝ) ^ r) ≤
      2 * Y * Real.exp (r * (1 + Real.log (((D + 1) * S) / Real.log X)) *
        (Real.log X) ^ (1 / 16 : ℝ) + C * Real.log (1 + Real.log (Real.sqrt Y))) := by
…

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

theorem OAI.Problem337.eventually_large_class_moment_bound_exp line 106

Source documentation

Exponential-cutoff form of the same complete class budget.

theorem eventually_large_class_moment_bound_exp (D r : ℝ) (hD : 1 ≤ D) (hr : 0 ≤ r) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ S : ℝ in atTop, ∀ v Y : ℝ, ∀ N : ℕ,
      S / (2 * Real.log S) ≤ v → v ≤ D * S →
      Real.exp (v / 2) ≤ Y → Y ≤ Real.exp v → (N : ℝ) ≤ Real.exp (D * S) →
      (∑ h ∈ (Finset.Icc 1 ⌊Y⌋₊).filter
        (fun h => DivisorClasses.LargeClass (N + h) v Y),
        (truncatedDivisorCount (Real.exp v) (N + h) : ℝ) ^ r) ≤
      2 * Y * Real.exp (r * (1 + Real.log (((D + 1) * S) / v)) *
        v ^ (1 / 16 : ℝ) + C * Real.log (1 + Real.log (Real.sqrt Y))) := by
…

Mentions: OAI.Problem337.D, OAI.Problem337.v, OAI.Problem337.DivisorClasses.LargeClass, OAI.Problem337.truncatedDivisorCount