HarmonicPrefixBudget.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.DivisorMoment.harmonic_prefix_budget line 10

Source documentation

Summing a harmonic divisor majorant over selected short-interval prefixes.

theorem harmonic_prefix_budget (r : ℝ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (N Y : ℕ) (A : Finset ℕ) (Z H : ℝ) (w : ℕ → ℝ),
      2 ≤ Z → ⌊Z⌋₊ ≤ Y → A ⊆ Finset.Ioc N (N + Y) →
      (∀ n ∈ A, ∃ d : ℕ, 0 < d ∧ (d : ℝ) ≤ Z ∧ d ∣ n ∧
        w n ≤ Real.exp H * (d.divisors.card : ℝ) ^ r) →
      (∑ n ∈ A, w n) ≤
        2 * (Y : ℝ) * Real.exp (H + C * Real.log (1 + Real.log Z)) := by
…

theorem OAI.Problem337.DivisorMoment.shifted_harmonic_prefix_budget line 48

Source documentation

The same estimate indexed by the positive translation parameter h.

theorem shifted_harmonic_prefix_budget (r : ℝ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (N Y : ℕ) (A : Finset ℕ) (Z H : ℝ) (w : ℕ → ℝ),
      2 ≤ Z → ⌊Z⌋₊ ≤ Y → A ⊆ Finset.Icc 1 Y →
      (∀ h ∈ A, ∃ d : ℕ, 0 < d ∧ (d : ℝ) ≤ Z ∧ d ∣ N + h ∧
        w h ≤ Real.exp H * (d.divisors.card : ℝ) ^ r) →
      (∑ h ∈ A, w h) ≤
        2 * (Y : ℝ) * Real.exp (H + C * Real.log (1 + Real.log Z)) := by
…

theorem OAI.Problem337.DivisorMoment.real_shifted_harmonic_prefix_budget line 73

Source documentation

The shifted prefix budget with the manuscript's real-valued interval length.

theorem real_shifted_harmonic_prefix_budget (r : ℝ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (N : ℕ) (Y : ℝ) (A : Finset ℕ) (Z H : ℝ) (w : ℕ → ℝ),
      2 ≤ Z → Z ≤ Y → A ⊆ Finset.Icc 1 ⌊Y⌋₊ →
      (∀ h ∈ A, ∃ d : ℕ, 0 < d ∧ (d : ℝ) ≤ Z ∧ d ∣ N + h ∧
        w h ≤ Real.exp H * (d.divisors.card : ℝ) ^ r) →
      (∑ h ∈ A, w h) ≤
        2 * Y * Real.exp (H + C * Real.log (1 + Real.log Z)) := by
…