OAI/NumberTheory/EgyptianFractions/RankinAdmissibility.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.rankin_band_exponent_admissible line 9

   Source documentation

   The intermediate-band Rankin exponent is admissible throughout the scale window.

   theorem rankin_band_exponent_admissible (S v t : ℝ)
       (hS : 1 < S) (ht : 1 ≤ t) (htv : t ≤ v)
       (hv : v ≤ S ^ 2) (hlow : 4 * Real.log S ≤ t) :
       Real.log (v / t) / (10 * t) ≤ 1 / 4 := by
   …

   Mentions: OAI.Problem337.v

2. theorem OAI.Problem337.divisor_rankin_intermediate_band_of_scale line 25

   Source documentation

   Evaluated Rankin estimate with its exponent restriction discharged by scale bounds.

   theorem divisor_rankin_intermediate_band_of_scale (r : ℕ) :
       ∃ C : ℝ, 0 < C ∧ ∀ S v t : ℝ, 1 < S → 1 ≤ t → t ≤ v →
         v ≤ S ^ 2 → 4 * Real.log S ≤ t → ∀ 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