HarmonicMoment.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.DivisorMoment.harmonic_divisor_moment_of_local_and_primes line 12

Source documentation

Finite Euler products combine uniform local control with a prime reciprocal bound.

theorem harmonic_divisor_moment_of_local_and_primes (r : ℕ) (C B : ℝ)
    (hC : 0 < C) (hB : 0 < B)
    (hlocal : ∀ p : ℕ, p.Prime → ∀ L : ℕ,
      Real.log (∑ j ∈ Finset.range (L + 1),
        (j + 1 : ℝ) ^ r * ((p : ℝ)⁻¹) ^ j) ≤ C / p)
    (hprimes : ∀ T : ℕ, 2 ≤ T →
      (∑ p ∈ T.factorial.primeFactors, (1 : ℝ) / p) ≤
        B * Real.log (1 + Real.log (T : ℝ))) :
    ∃ A : ℝ, 0 < A ∧ ∀ T : ℕ, 2 ≤ T →
      (∑ n ∈ Finset.Icc 1 T, (n.divisors.card : ℝ) ^ r / n) ≤
        Real.exp (A * Real.log (1 + Real.log (T : ℝ))) := by
…

theorem OAI.Problem337.DivisorMoment.factorial_primeFactors_eq_primesLE line 34
Source documentation
The prime factors of a factorial are exactly the primes up to its index.
```
theorem factorial_primeFactors_eq_primesLE (T : ℕ) :
    T.factorial.primeFactors = Nat.primesLE T := by
…
```

theorem OAI.Problem337.DivisorMoment.harmonic_divisor_moment_bound line 47

Source documentation

An unconditional harmonic divisor-moment bound, with a constant depending only on r.

theorem harmonic_divisor_moment_bound (r : ℕ) :
    ∃ A : ℝ, 0 < A ∧ ∀ T : ℕ, 2 ≤ T →
      (∑ n ∈ Finset.Icc 1 T, (n.divisors.card : ℝ) ^ r / n) ≤
        Real.exp (A * Real.log (1 + Real.log (T : ℝ))) := by
…

theorem OAI.Problem337.DivisorMoment.harmonic_divisor_real_moment_bound line 62

Source documentation

Arbitrary real moments follow by increasing the moment to a natural number.

theorem harmonic_divisor_real_moment_bound (r : ℝ) :
    ∃ A : ℝ, 0 < A ∧ ∀ T : ℕ, 2 ≤ T →
      (∑ n ∈ Finset.Icc 1 T, (n.divisors.card : ℝ) ^ r / n) ≤
        Real.exp (A * Real.log (1 + Real.log (T : ℝ))) := by
…

theorem OAI.Problem337.DivisorMoment.harmonic_divisor_moment_real_cutoff line 80

Source documentation

Real cutoffs are allowed, as in the uniform divisor-moment estimate.

theorem harmonic_divisor_moment_real_cutoff (r : ℝ) :
    ∃ A : ℝ, 0 < A ∧ ∀ X : ℝ, 2 ≤ X →
      (∑ n ∈ Finset.Icc 1 ⌊X⌋₊, (n.divisors.card : ℝ) ^ r / n) ≤
        Real.exp (A * Real.log (1 + Real.log X)) := by
…