LargePrefixHarmonic.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.large_prefix_class_harmonic_bound line 12

Source documentation

The actual large-prefix class has an unconditional harmonic-moment budget. The finite set is indexed by the positive translation parameter.

theorem large_prefix_class_harmonic_bound (r : ℝ) (hr : 0 ≤ r) :
    ∃ C : ℝ, 0 < C ∧ ∀ (X W Z L Y : ℝ) (N : ℕ) (A : Finset ℕ),
      1 < X → Real.log X ≤ W → 0 < L → 2 ≤ Z → Z ≤ Y →
      A ⊆ Finset.Icc 1 ⌊Y⌋₊ →
      (∀ h ∈ A, Real.log ((N + h : ℕ) : ℝ) ≤ W) →
      (∀ h ∈ A, InLargePrefixClass Z L (N + h)) →
      (∑ h ∈ A, (truncatedDivisorCount X (N + h) : ℝ) ^ r) ≤
        2 * Y * Real.exp (r * ((1 + Real.log (W / Real.log X)) * Real.log X / L) +
          C * Real.log (1 + Real.log Z)) := by
…

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

theorem OAI.Problem337.large_prefix_class_sqrt_harmonic_bound line 37

Source documentation

The manuscript's square-root cutoff and large-next-prime threshold, with the harmonic divisor sum fully discharged.

theorem large_prefix_class_sqrt_harmonic_bound (r : ℝ) (hr : 0 ≤ r) :
    ∃ C : ℝ, 0 < C ∧ ∀ (X W Y : ℝ) (N : ℕ) (A : Finset ℕ),
      1 < X → Real.log X ≤ W → 4 ≤ Y →
      A ⊆ Finset.Icc 1 ⌊Y⌋₊ →
      (∀ h ∈ A, Real.log ((N + h : ℕ) : ℝ) ≤ W) →
      (∀ 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 : ℝ) +
          C * Real.log (1 + Real.log (Real.sqrt Y))) := by
…

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