OAI/NumberTheory/EgyptianFractions/RankinBand.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Problem337.uniform_divisor_smooth_rankin_loglog_boundline 12Source documentation
Smooth harmonic divisor tails with all Euler and prime sums evaluated.
theorem uniform_divisor_smooth_rankin_loglog_bound (r : ℕ) : ∃ C : ℝ, 0 < C ∧ ∀ β V W : ℝ, 0 ≤ β → β ≤ 1 / 4 → 1 ≤ W → ∀ N : ℕ, (∀ p ∈ N.primesBelow, (p : ℝ) ≤ Real.exp W) → ∀ s : Finset ℕ, (∀ n ∈ s, n ∈ N.smoothNumbers) → (∀ n ∈ s, Real.exp V ≤ (n : ℝ)) → (∑ n ∈ s, (n.divisors.card : ℝ) ^ r / (n : ℝ)) ≤ Real.exp (-β * V + C * Real.exp (β * W) * Real.log (1 + W)) := by … - theorem
OAI.Problem337.divisor_rankin_intermediate_bandline 36Source documentation
The exact intermediate-prime-band Rankin estimate. The only scale restriction is the explicit admissibility of the chosen Rankin exponent.
theorem divisor_rankin_intermediate_band (r : ℕ) : ∃ C : ℝ, 0 < C ∧ ∀ v t : ℝ, 1 ≤ t → t ≤ v → Real.log (v / t) / (10 * t) ≤ 1 / 4 → ∀ N : ℕ, (∀ p ∈ N.primesBelow, (p : ℝ) ≤ Real.exp (2 * t)) → ∀ s : Finset ℕ, (∀ n ∈ s, n ∈ N.smoothNumbers) → (∀ n ∈ s, Real.exp (v / 5) ≤ (n : ℝ)) → (∑ n ∈ s, (n.divisors.card : ℝ) ^ r / (n : ℝ)) ≤ Real.exp (-(v / t) * Real.log (v / t) / 50 + C * (v / t) ^ (1 / 5 : ℝ) * Real.log (2 * t)) := by …Mentions: OAI.Problem337.v
- theorem
OAI.Problem337.divisor_rankin_intermediate_band_of_prime_divisorsline 63Source documentation
A real-cutoff version avoiding any rounding obligation at the call site.
theorem divisor_rankin_intermediate_band_of_prime_divisors (r : ℕ) : ∃ C : ℝ, 0 < C ∧ ∀ v t : ℝ, 1 ≤ t → t ≤ v → Real.log (v / t) / (10 * t) ≤ 1 / 4 → ∀ s : Finset ℕ, (∀ n ∈ s, ∀ p : ℕ, p.Prime → p ∣ n → (p : ℝ) ≤ Real.exp (2 * t)) → (∀ n ∈ s, Real.exp (v / 5) ≤ (n : ℝ)) → (∑ n ∈ s, (n.divisors.card : ℝ) ^ r / (n : ℝ)) ≤ Real.exp (-(v / t) * Real.log (v / t) / 50 + C * (v / t) ^ (1 / 5 : ℝ) * Real.log (2 * t)) := by …Mentions: OAI.Problem337.v