VaughanDyadicDecomposition.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.Vaughan.long_hyperbola_eq_filtered_product line 12
def OAI.Problem337.Vaughan.typeIIBlock line 26
Source documentation
The dyadic block with the actual arithmetic coefficients in Vaughan's identity.
```
def typeIIBlock (N U V j : ℕ) (w : ℕ → ℂ) : ℂ :=
…
```
theorem OAI.Problem337.Vaughan.typeII_eq_sum_dyadic_blocks line 31
Source documentation
No arithmetic coefficient or hyperbolic cutoff is lost in dyadic decomposition.
```
theorem typeII_eq_sum_dyadic_blocks (N U V : ℕ) (w : ℕ → ℂ) :
    weightedSum (Ioc 0 N) w (typeIICoefficient U * longPart V Λ) =
      ∑ j ∈ range (Nat.log 2 N + 1), typeIIBlock N U V j w := by
…
```
Mentions: OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.Vaughan.typeIICoefficient, OAI.Problem337.Vaughan.longPart, OAI.Problem337.Vaughan.typeIIBlock
theorem OAI.Problem337.Vaughan.norm_typeII_le_sum_dyadic_blocks line 38
theorem OAI.Problem337.Vaughan.norm_typeII_le_dyadic_log_budget line 45
Source documentation
A genuine uniform block bound has only a logarithmic decomposition cost.
```
theorem norm_typeII_le_dyadic_log_budget (N U V : ℕ) (w : ℕ → ℂ)
    (B : ℝ) (hB0 : 0 ≤ B)
    (hB : ∀ j < Nat.log 2 N + 1, ‖typeIIBlock N U V j w‖ ≤ B) :
    ‖weightedSum (Ioc 0 N) w (typeIICoefficient U * longPart V Λ)‖ ≤
      (1 + Real.log N / Real.log 2) * B := by
…
```
Mentions: OAI.Problem337.Vaughan.typeIIBlock, OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.Vaughan.typeIICoefficient, OAI.Problem337.Vaughan.longPart

theorem OAI.Problem337.Vaughan.norm_vonMangoldt_sum_le_dyadic line 61

Source documentation

The complete finite Vaughan envelope, with its Type II term split into actual dyadic blocks ready for interval correlation estimates.

theorem norm_vonMangoldt_sum_le_dyadic (N U V : ℕ) (w : ℕ → ℂ) (B₁ B₂ : ℕ → ℝ)
    (hw : ∀ n ∈ Ioc 0 N, ‖w n‖ ≤ 1)
    (hfirst : ∀ a ∈ Ioc 0 (min U N), ∀ k ≤ N / a,
      ‖∑ b ∈ Ioc 0 k, w (a * b)‖ ≤ B₁ a)
    (hsecond : ∀ a ∈ Ioc 0 (min (U * V) N),
      ‖∑ b ∈ Ioc 0 (N / a), w (a * b)‖ ≤ B₂ a) :
    ‖weightedSum (Ioc 0 N) w Λ‖ ≤
      (V : ℝ) * Real.log V +
      2 * Real.log N * (∑ a ∈ Ioc 0 (min U N), B₁ a) +
      Real.log N * (∑ a ∈ Ioc 0 (min (U * V) N), B₂ a) +
      ∑ j ∈ range (Nat.log 2 N + 1), ‖typeIIBlock N U V j w‖ := by
…

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

theorem OAI.Problem337.Vaughan.typeII_shell_energy_le line 77
Source documentation
Sharp unconditional row energy for the actual Type II coefficient in a dyadic shell.
```
theorem typeII_shell_energy_le (N U j : ℕ) :
    (∑ m ∈ VaughanDyadic.shell U N j, ‖(typeIICoefficient U m : ℂ)‖ ^ 2) ≤
      (2 ^ (j + 1) : ℕ) * (1 + Real.log (2 ^ (j + 1) : ℕ)) ^ 3 := by
…
```
Mentions: OAI.Problem337.VaughanDyadic.shell, OAI.Problem337.Vaughan.typeIICoefficient