OAI/NumberTheory/EgyptianFractions/VaughanTypeI.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem337.Vaughan.sum_Ioc_zero_eq_sum_range_succ line 11

   Source documentation

   Indexing positive initial intervals by a zero-based range.

   lemma sum_Ioc_zero_eq_sum_range_succ {R : Type*} [AddCommMonoid R]
       (f : ℕ → R) (N : ℕ) :
       (∑ j ∈ Finset.Ioc 0 N, f j) = ∑ j ∈ Finset.range N, f (j + 1) := by
   …

2. theorem OAI.Problem337.Vaughan.log_weighted_sum_norm_le line 21

   Source documentation

   Adding a logarithmic weight costs at most twice the endpoint logarithm. The prefix bound remains explicit; no cancellation estimate is assumed silently.

   theorem log_weighted_sum_norm_le (w : ℕ → ℂ) (N : ℕ) (B : ℝ)
       (hprefix : ∀ k ≤ N, ‖∑ j ∈ Finset.Ioc 0 k, w j‖ ≤ B) :
       ‖∑ j ∈ Finset.Ioc 0 N, (Real.log j : ℂ) * w j‖ ≤
         2 * B * Real.log N := by
   …

3. theorem OAI.Problem337.Vaughan.norm_log_bilinear_sum_le line 56

   Source documentation

   Type I logarithmic bilinear estimate for coefficients bounded by one.

   theorem norm_log_bilinear_sum_le (w : ℕ → ℂ) (N A : ℕ) (c B : ℕ → ℝ)
       (hA : A ≤ N)
       (hc : ∀ a ∈ Finset.Ioc 0 A, |c a| ≤ 1)
       (hprefix : ∀ a ∈ Finset.Ioc 0 A, ∀ k ≤ N / a,
         ‖∑ b ∈ Finset.Ioc 0 k, w (a * b)‖ ≤ B a) :
       ‖∑ a ∈ Finset.Ioc 0 A, (c a : ℂ) *
           ∑ b ∈ Finset.Ioc 0 (N / a), (Real.log b : ℂ) * w (a * b)‖ ≤
         2 * Real.log N * ∑ a ∈ Finset.Ioc 0 A, B a := by
   …

4. theorem OAI.Problem337.Vaughan.norm_bilinear_sum_le_log line 92

   Source documentation

   Type I bilinear estimate for coefficients with the logarithmic majorant.

   theorem norm_bilinear_sum_le_log (w : ℕ → ℂ) (N A : ℕ) (c B : ℕ → ℝ)
       (hA : A ≤ N)
       (hc : ∀ a ∈ Finset.Ioc 0 A, |c a| ≤ Real.log a)
       (hinner : ∀ a ∈ Finset.Ioc 0 A,
         ‖∑ b ∈ Finset.Ioc 0 (N / a), w (a * b)‖ ≤ B a) :
       ‖∑ a ∈ Finset.Ioc 0 A, (c a : ℂ) *
           ∑ b ∈ Finset.Ioc 0 (N / a), w (a * b)‖ ≤
         Real.log N * ∑ a ∈ Finset.Ioc 0 A, B a := by
   …

5. theorem OAI.Problem337.Vaughan.first_typeI_sum_bound line 116

   Source documentation

   The first Vaughan Type I term in its finite bilinear form.

   theorem first_typeI_sum_bound (w : ℕ → ℂ) (N U : ℕ) (B : ℕ → ℝ)
       (hprefix : ∀ a ∈ Finset.Ioc 0 (min U N), ∀ k ≤ N / a,
         ‖∑ b ∈ Finset.Ioc 0 k, w (a * b)‖ ≤ B a) :
       ‖∑ a ∈ Finset.Ioc 0 (min U N), ((μ a : ℝ) : ℂ) *
           ∑ b ∈ Finset.Ioc 0 (N / a), (Real.log b : ℂ) * w (a * b)‖ ≤
         2 * Real.log N * ∑ a ∈ Finset.Ioc 0 (min U N), B a := by
   …

6. theorem OAI.Problem337.Vaughan.second_typeI_sum_bound line 128

   Source documentation

   The second Vaughan Type I term in its finite bilinear form.

   theorem second_typeI_sum_bound (w : ℕ → ℂ) (N U V : ℕ) (B : ℕ → ℝ)
       (hinner : ∀ a ∈ Finset.Ioc 0 (min (U * V) N),
         ‖∑ b ∈ Finset.Ioc 0 (N / a), w (a * b)‖ ≤ B a) :
       ‖∑ a ∈ Finset.Ioc 0 (min (U * V) N), (typeICoefficient U V a : ℂ) *
           ∑ b ∈ Finset.Ioc 0 (N / a), w (a * b)‖ ≤
         Real.log N * ∑ a ∈ Finset.Ioc 0 (min (U * V) N), B a := by
   …

   Mentions: OAI.Problem337.Vaughan.typeICoefficient

7. theorem OAI.Problem337.Vaughan.first_typeI_bound line 138

   Source documentation

   First Type I estimate directly for the actual Vaughan convolution.

   theorem first_typeI_bound (w : ℕ → ℂ) (N U : ℕ) (B : ℕ → ℝ)
       (hprefix : ∀ a ∈ Finset.Ioc 0 (min U N), ∀ k ≤ N / a,
         ‖∑ b ∈ Finset.Ioc 0 k, w (a * b)‖ ≤ B a) :
       ‖weightedSum (Finset.Ioc 0 N) w
           (shortPart U (μ : ArithmeticFunction ℝ) * ArithmeticFunction.log)‖ ≤
         2 * Real.log N * ∑ a ∈ Finset.Ioc 0 (min U N), B a := by
   …

   Mentions: OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.Vaughan.shortPart

8. theorem OAI.Problem337.Vaughan.second_typeI_bound line 148

   Source documentation

   Second Type I estimate directly for the actual Vaughan convolution.

   theorem second_typeI_bound (w : ℕ → ℂ) (N U V : ℕ) (B : ℕ → ℝ)
       (hinner : ∀ a ∈ Finset.Ioc 0 (min (U * V) N),
         ‖∑ b ∈ Finset.Ioc 0 (N / a), w (a * b)‖ ≤ B a) :
       ‖weightedSum (Finset.Ioc 0 N) w (typeICoefficient U V * ζ)‖ ≤
         Real.log N * ∑ a ∈ Finset.Ioc 0 (min (U * V) N), B a := by
   …

   Mentions: OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.Vaughan.typeICoefficient