OAI/NumberTheory/EgyptianFractions/IntermediatePrimeClass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.DivisorMoment.sum_le_shifted_divisor_majorant_real_cutoff line 10

   Source documentation

   Prefix counting in the shift convention used by short-interval moments.

   theorem sum_le_shifted_divisor_majorant_real_cutoff
       (N : ℕ) (Y : ℝ) (H D : Finset ℕ) (w a : ℕ → ℝ) (hY : 0 ≤ Y)
       (hH : H ⊆ Finset.Icc 1 ⌊Y⌋₊)
       (hassign : ∀ h ∈ H, ∃ d ∈ D, d ∣ N + h ∧ w h ≤ a d)
       (ha : ∀ d ∈ D, 0 ≤ a d)
       (hD : ∀ d ∈ D, 0 < d ∧ (d : ℝ) ≤ Y) :
       (∑ h ∈ H, w h) ≤ 2 * Y * ∑ d ∈ D, a d / d := by
   …

   Mentions: OAI.Problem337.D

2. theorem OAI.Problem337.DivisorMoment.intermediate_prime_class_bound line 39

   Source documentation

   One actual intermediate-prime class, with all divisor-prefix counting and smooth Rankin summation performed. Only the pointwise prefix witnesses remain as hypotheses; no moment or counting estimate is assumed.

   theorem intermediate_prime_class_bound (r : ℕ) :
       ∃ C : ℝ, 0 < C ∧ ∀ (N : ℕ) (Y v t R : ℝ) (H : Finset ℕ) (w : ℕ → ℝ),
         0 ≤ Y → 1 ≤ t → t ≤ v → Real.log (v / t) / (10 * t) ≤ 1 / 4 →
         H ⊆ Finset.Icc 1 ⌊Y⌋₊ →
         (∀ h ∈ H, ∃ d : ℕ, d ∣ N + h ∧ (d : ℝ) ≤ Y ∧
           Real.exp (v / 5) ≤ (d : ℝ) ∧
           (∀ p : ℕ, p.Prime → p ∣ d → (p : ℝ) ≤ Real.exp (2 * t)) ∧
           w h ≤ Real.exp R * (d.divisors.card : ℝ) ^ r) →
         (∑ h ∈ H, w h) ≤ 2 * Y *
           Real.exp (R - (v / t) * Real.log (v / t) / 50 +
             C * (v / t) ^ (1 / 5 : ℝ) * Real.log (2 * t)) := by
   …

   Mentions: OAI.Problem337.v

3. theorem OAI.Problem337.DivisorMoment.intermediate_prime_class_bound_real line 104

   Source documentation

   The same evaluated class estimate for arbitrary real moment orders.

   theorem intermediate_prime_class_bound_real (r : ℝ) :
       ∃ C : ℝ, 0 < C ∧ ∀ (N : ℕ) (Y v t R : ℝ) (H : Finset ℕ) (w : ℕ → ℝ),
         0 ≤ Y → 1 ≤ t → t ≤ v → Real.log (v / t) / (10 * t) ≤ 1 / 4 →
         H ⊆ Finset.Icc 1 ⌊Y⌋₊ →
         (∀ h ∈ H, ∃ d : ℕ, d ∣ N + h ∧ (d : ℝ) ≤ Y ∧
           Real.exp (v / 5) ≤ (d : ℝ) ∧
           (∀ p : ℕ, p.Prime → p ∣ d → (p : ℝ) ≤ Real.exp (2 * t)) ∧
           w h ≤ Real.exp R * (d.divisors.card : ℝ) ^ r) →
         (∑ h ∈ H, w h) ≤ 2 * Y *
           Real.exp (R - (v / t) * Real.log (v / t) / 50 +
             C * (v / t) ^ (1 / 5 : ℝ) * Real.log (2 * t)) := by
   …

   Mentions: OAI.Problem337.v

4. theorem OAI.Problem337.DivisorMoment.intermediate_prime_class_sqrt_bound line 132

   Source documentation

   The prefix cutoff sqrt Y used in the actual prime-factor decomposition is directly admissible. The arbitrary loss R can be instantiated by r*B*v/t.

   theorem intermediate_prime_class_sqrt_bound (r : ℝ) :
       ∃ C : ℝ, 0 < C ∧ ∀ (N : ℕ) (Y v t R : ℝ) (H : Finset ℕ) (w : ℕ → ℝ),
         1 ≤ Y → 1 ≤ t → t ≤ v → Real.log (v / t) / (10 * t) ≤ 1 / 4 →
         H ⊆ Finset.Icc 1 ⌊Y⌋₊ →
         (∀ h ∈ H, ∃ d : ℕ, d ∣ N + h ∧ (d : ℝ) ≤ Real.sqrt Y ∧
           Real.exp (v / 5) ≤ (d : ℝ) ∧
           (∀ p : ℕ, p.Prime → p ∣ d → (p : ℝ) ≤ Real.exp (2 * t)) ∧
           w h ≤ Real.exp R * (d.divisors.card : ℝ) ^ r) →
         (∑ h ∈ H, w h) ≤ 2 * Y *
           Real.exp (R - (v / t) * Real.log (v / t) / 50 +
             C * (v / t) ^ (1 / 5 : ℝ) * Real.log (2 * t)) := by
   …

   Mentions: OAI.Problem337.v