LargePrefixClass.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.InLargePrefixClass line 12
Source documentation
The large-prime class, including integers already below the prefix cutoff. The existential witnesses need not be chosen canonically.
```
def InLargePrefixClass (Z L : ℝ) (n : ℕ) : Prop :=
…
```

theorem OAI.Problem337.large_prefix_class_majorant line 18

Source documentation

Each member of the large-prime class has a divisor-indexed moment majorant.

theorem large_prefix_class_majorant (X W r Z L : ℝ) {n : ℕ}
    (hn : 0 < n) (hX : 1 < X) (hXW : Real.log X ≤ W)
    (hnW : Real.log (n : ℝ) ≤ W) (hr : 0 ≤ r) (hL : 0 < L)
    (hclass : InLargePrefixClass Z L n) :
    ∃ d : ℕ, 0 < d ∧ d ∣ n ∧ (d : ℝ) ≤ Z ∧
      (truncatedDivisorCount X n : ℝ) ^ r ≤ (d.divisors.card : ℝ) ^ r *
        Real.exp (r * ((1 + Real.log (W / Real.log X)) * Real.log X / L)) := by
…

Mentions: OAI.Problem337.InLargePrefixClass, OAI.Problem337.truncatedDivisorCount

theorem OAI.Problem337.large_prefix_class_moment_bound line 58

Source documentation

Actual weighted sum over the large-prime class in a translated real interval.

theorem large_prefix_class_moment_bound (X W r Z L Y : ℝ) (N : ℕ) (A : Finset ℕ)
    (hX : 1 < X) (hXW : Real.log X ≤ W) (hr : 0 ≤ r) (hL : 0 < L)
    (hZ : 1 ≤ Z) (hZY : Z ≤ Y)
    (hA : A ⊆ Finset.Ioc N (N + ⌊Y⌋₊))
    (hW : ∀ n ∈ A, Real.log (n : ℝ) ≤ W)
    (hclass : ∀ n ∈ A, InLargePrefixClass Z L n) :
    (∑ n ∈ A, (truncatedDivisorCount X n : ℝ) ^ r) ≤
      2 * Y * Real.exp (r * ((1 + Real.log (W / Real.log X)) * Real.log X / L)) *
        ∑ d ∈ Finset.Icc 1 ⌊Z⌋₊, (d.divisors.card : ℝ) ^ r / d := by
…

Mentions: OAI.Problem337.InLargePrefixClass, OAI.Problem337.truncatedDivisorCount

theorem OAI.Problem337.large_prefix_class_sqrt_moment_bound line 97

Source documentation

The manuscript's large-prime estimate, with threshold (log X)^(15/16).

theorem large_prefix_class_sqrt_moment_bound (X W r Y : ℝ) (N : ℕ) (A : Finset ℕ)
    (hX : 1 < X) (hXW : Real.log X ≤ W) (hr : 0 ≤ r) (hY : 1 ≤ Y)
    (hA : A ⊆ Finset.Ioc N (N + ⌊Y⌋₊))
    (hW : ∀ n ∈ A, Real.log (n : ℝ) ≤ W)
    (hclass : ∀ n ∈ A, InLargePrefixClass (Real.sqrt Y) ((Real.log X) ^ (15 / 16 : ℝ)) n) :
    (∑ n ∈ A, (truncatedDivisorCount X n : ℝ) ^ r) ≤
      2 * Y * Real.exp (r * (1 + Real.log (W / Real.log X)) * (Real.log X) ^ (1 / 16 : ℝ)) *
        ∑ d ∈ Finset.Icc 1 ⌊Real.sqrt Y⌋₊, (d.divisors.card : ℝ) ^ r / d := by
…

Mentions: OAI.Problem337.InLargePrefixClass, OAI.Problem337.truncatedDivisorCount

theorem OAI.Problem337.large_prefix_class_shifted_sqrt_moment_bound line 124

Source documentation

Shifted-index version, matching the uniform short-interval moment statement.

theorem large_prefix_class_shifted_sqrt_moment_bound (X W r Y : ℝ) (N : ℕ) (A : Finset ℕ)
    (hX : 1 < X) (hXW : Real.log X ≤ W) (hr : 0 ≤ r) (hY : 1 ≤ Y)
    (hA : A ⊆ Finset.Icc 1 ⌊Y⌋₊)
    (hW : ∀ h ∈ A, Real.log ((N + h : ℕ) : ℝ) ≤ W)
    (hclass : ∀ h ∈ A, InLargePrefixClass (Real.sqrt Y)
      ((Real.log X) ^ (15 / 16 : ℝ)) (N + h)) :
    (∑ h ∈ A, (truncatedDivisorCount X (N + h) : ℝ) ^ r) ≤
      2 * Y * Real.exp (r * (1 + Real.log (W / Real.log X)) * (Real.log X) ^ (1 / 16 : ℝ)) *
        ∑ d ∈ Finset.Icc 1 ⌊Real.sqrt Y⌋₊, (d.divisors.card : ℝ) ^ r / d := by
…

Mentions: OAI.Problem337.InLargePrefixClass, OAI.Problem337.truncatedDivisorCount