LogWeightedSums.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic weights in finite exponential sums

Abel summation transfers a uniform bound for all prefixes of a sequence to its logarithmically weighted sum. This supplies the inner logarithmic weight in the first Type I term of Vaughan's identity; no estimate over primes is assumed here.

theorem OAI.Problem337.Vaughan.norm_sum_smul_le_two_mul_of_monotone line 20

Source documentation

An increasing nonnegative real weight costs at most twice its endpoint when all unweighted prefix sums are bounded by B.

theorem norm_sum_smul_le_two_mul_of_monotone
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (f : ℕ → ℝ) (z : ℕ → E) (N : ℕ) (B : ℝ)
    (hf : Monotone f) (hf0 : 0 ≤ f 0)
    (hprefix : ∀ k ≤ N + 1, ‖∑ j ∈ Finset.range k, z j‖ ≤ B) :
    ‖∑ j ∈ Finset.range (N + 1), f j • z j‖ ≤ 2 * f N * B := by
…

theorem OAI.Problem337.Vaughan.norm_log_weighted_range_le line 53

Source documentation

Logarithmic weights on positive indices, in shifted-range form. The result also holds for N = 0 and N = 1, when the weighted sum is zero.

theorem norm_log_weighted_range_le
    (z : ℕ → ℂ) (N : ℕ) (B : ℝ)
    (hprefix : ∀ k ≤ N, ‖∑ j ∈ Finset.range k, z (j + 1)‖ ≤ B) :
    ‖∑ j ∈ Finset.range N, (Real.log (j + 1 : ℕ) : ℂ) * z (j + 1)‖ ≤
      2 * Real.log N * B := by
…

lemma OAI.Problem337.Vaughan.sum_Icc_one_eq_shifted_range line 71

theorem OAI.Problem337.Vaughan.norm_log_weighted_Icc_le line 79

Source documentation

Positive-interval formulation of the logarithmic Abel estimate.

theorem norm_log_weighted_Icc_le
    (z : ℕ → ℂ) (N : ℕ) (B : ℝ)
    (hprefix : ∀ k ≤ N, ‖∑ j ∈ Finset.Icc 1 k, z j‖ ≤ B) :
    ‖∑ j ∈ Finset.Icc 1 N, (Real.log j : ℂ) * z j‖ ≤
      2 * Real.log N * B := by
…