OAI/NumberTheory/EgyptianFractions/PrimeFourierDeweight.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.norm_sum_range_weighted_le_of_partial_sums line 11

   Source documentation

   Finite Abel summation: a nonnegative decreasing weight does not enlarge a uniform partial-sum bound by more than its first value.

   theorem norm_sum_range_weighted_le_of_partial_sums
       (f : ℕ → ℝ) (g : ℕ → ℂ) (hf : ∀ i, 0 ≤ f i) (hmono : Antitone f)
       (n : ℕ) (B : ℝ) (hB : 0 ≤ B)
       (hpartial : ∀ k ≤ n, ‖∑ i ∈ Finset.range k, g i‖ ≤ B) :
       ‖∑ i ∈ Finset.range n, f i • g i‖ ≤ f 0 * B := by
   …

2. theorem OAI.Problem337.norm_prime_interval_sum_le_of_log_partial_sums line 43

   Source documentation

   Logarithmic prime weights may be removed on an interval at a cost of only 1 / log L, provided all weighted partial sums on that interval are bounded.

   theorem norm_prime_interval_sum_le_of_log_partial_sums
       (L n : ℕ) (hL : 2 ≤ L) (w : ℕ → ℂ) (B : ℝ) (hB : 0 ≤ B)
       (hpartial : ∀ k ≤ n,
         ‖∑ p ∈ Finset.Ico L (L + k), (primeLogWeight p : ℂ) * w p‖ ≤ B) :
       ‖∑ p ∈ (Finset.Ico L (L + n)).filter Nat.Prime, w p‖ ≤
         B / Real.log (L : ℝ) := by
   …

   Mentions: OAI.Problem337.primeLogWeight

3. theorem OAI.Problem337.norm_prime_sum_le_cutoff_add_log_bound line 80

   Source documentation

   A short initial segment plus Abel summation converts a uniform bound for prime-logarithmic prefix sums into an unweighted prime sum bound.

   theorem norm_prime_sum_le_cutoff_add_log_bound
       (L N : ℕ) (hL : 2 ≤ L) (hLN : L ≤ N) (w : ℕ → ℂ)
       (hw : ∀ p < L, ‖w p‖ ≤ 1) (B : ℝ) (hB : 0 ≤ B)
       (hpartial : ∀ k ≤ N,
         ‖∑ p ∈ Finset.range k, (primeLogWeight p : ℂ) * w p‖ ≤ B) :
       ‖∑ p ∈ (Finset.range N).filter Nat.Prime, w p‖ ≤
         (L : ℝ) + 2 * B / Real.log (L : ℝ) := by
   …

   Mentions: OAI.Problem337.primeLogWeight