VaughanDecomposition.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.Vaughan.weightedSum_shortPart line 10
Source documentation
Taking a short part restricts a finite weighted sum to the smaller interval.
```
theorem weightedSum_shortPart (N V : ℕ) (w : ℕ → ℂ) (f : ArithmeticFunction ℝ) :
    weightedSum (Finset.Ioc 0 N) w (shortPart V f) =
      weightedSum (Finset.Ioc 0 (min V N)) w f := by
…
```
Mentions: OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.Vaughan.shortPart
theorem OAI.Problem337.Vaughan.norm_short_vonMangoldt_sum_le line 32
Source documentation
The initial von Mangoldt segment has the elementary V log V bound.
```
theorem norm_short_vonMangoldt_sum_le (N V : ℕ) (w : ℕ → ℂ)
    (hw : ∀ n ∈ Finset.Ioc 0 N, ‖w n‖ ≤ 1) :
    ‖weightedSum (Finset.Ioc 0 N) w (shortPart V Λ)‖ ≤
      (V : ℝ) * Real.log V := by
…
```
Mentions: OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.Vaughan.shortPart
theorem OAI.Problem337.Vaughan.typeII_eq_hyperbola line 57
Source documentation
The actual Type II term is a hyperbola with both short factors removed.
```
theorem typeII_eq_hyperbola (N U V : ℕ) (w : ℕ → ℂ) :
    weightedSum (Finset.Ioc 0 N) w (typeIICoefficient U * longPart V Λ) =
      ∑ d ∈ (hyperbola N).filter (fun d => U < d.1 ∧ V < d.2),
        (typeIICoefficient U d.1 : ℂ) * (Λ d.2 : ℂ) * w (d.1 * d.2) := by
…
```
Mentions: OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.Vaughan.typeIICoefficient, OAI.Problem337.Vaughan.longPart, OAI.Problem337.Vaughan.hyperbola

theorem OAI.Problem337.Vaughan.norm_vonMangoldt_sum_le line 71

Source documentation

A fully finite Vaughan estimate. Only the displayed elementary inner-sum envelopes are hypotheses; the remaining Type II sum is retained explicitly.

theorem norm_vonMangoldt_sum_le (N U V : ℕ) (w : ℕ → ℂ) (B₁ B₂ : ℕ → ℝ)
    (hw : ∀ n ∈ Finset.Ioc 0 N, ‖w n‖ ≤ 1)
    (hfirst : ∀ a ∈ Finset.Ioc 0 (min U N), ∀ k ≤ N / a,
      ‖∑ b ∈ Finset.Ioc 0 k, w (a * b)‖ ≤ B₁ a)
    (hsecond : ∀ 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 Λ‖ ≤
      (V : ℝ) * Real.log V +
      2 * Real.log N * (∑ a ∈ Finset.Ioc 0 (min U N), B₁ a) +
      Real.log N * (∑ a ∈ Finset.Ioc 0 (min (U * V) N), B₂ a) +
      ‖∑ d ∈ (hyperbola N).filter (fun d => U < d.1 ∧ V < d.2),
        (typeIICoefficient U d.1 : ℂ) * (Λ d.2 : ℂ) * w (d.1 * d.2)‖ := by
…

Mentions: OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.Vaughan.hyperbola, OAI.Problem337.Vaughan.typeIICoefficient