VaughanDyadic.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Exact dyadic decomposition of a truncated hyperbola

The long--long convolution is partitioned into genuine dyadic row intervals. Each column interval is shortened to N / 2^j, retaining the exact mn ≤ N cutoff. This is a finite reindexing, with no analytic cancellation hypothesis.

def OAI.Problem337.VaughanDyadic.shell line 19
Source documentation
Rows above the lower cutoff, inside one half-open power-of-two interval.
```
def shell (U N j : ℕ) : Finset ℕ :=
…
```
lemma OAI.Problem337.VaughanDyadic.mem_shell line 22
lemma OAI.Problem337.VaughanDyadic.shell_eq_log_fiber line 27
lemma OAI.Problem337.VaughanDyadic.shell_eq_Icc line 37
Source documentation
The shell is a single consecutive interval, so its phase correlations remain geometric.
```
lemma shell_eq_Icc (U N j : ℕ) :
    shell U N j = Icc (max (U + 1) (2 ^ j)) (min N (2 ^ (j + 1) - 1)) := by
…
```
Mentions: OAI.Problem337.VaughanDyadic.shell

theorem OAI.Problem337.VaughanDyadic.sum_eq_sum_shells line 46

Source documentation

Exact partition, valid also when the original interval is empty.

theorem sum_eq_sum_shells {E : Type*} [AddCommMonoid E]
    (U N : ℕ) (f : ℕ → E) :
    (∑ m ∈ Ioc U N, f m) =
      ∑ j ∈ range (Nat.log 2 N + 1), ∑ m ∈ shell U N j, f m := by
…

Mentions: OAI.Problem337.VaughanDyadic.shell

lemma OAI.Problem337.VaughanDyadic.inner_sum_eq_common_cutoff line 55
def OAI.Problem337.VaughanDyadic.block line 76
Source documentation
The actual dyadic block, not a rectangular surrogate without the cutoff.
```
def block {E : Type*} [AddCommMonoid E] (N U V j : ℕ) (F : ℕ → ℕ → E) : E :=
…
```
Mentions: OAI.Problem337.F

theorem OAI.Problem337.VaughanDyadic.sum_hyperbola_eq_sum_blocks line 81

Source documentation

Exact long--long hyperbola decomposition into common-column dyadic blocks.

theorem sum_hyperbola_eq_sum_blocks {E : Type*} [AddCommMonoid E]
    (N U V : ℕ) (F : ℕ → ℕ → E) :
    (∑ m ∈ Ioc U N, ∑ n ∈ Ioc V (N / m), F m n) =
      ∑ j ∈ range (Nat.log 2 N + 1), block N U V j F := by
…

Mentions: OAI.Problem337.F, OAI.Problem337.VaughanDyadic.block

theorem OAI.Problem337.VaughanDyadic.sum_filtered_product_eq_sum_blocks line 94

Source documentation

Product-finset form of the same exact decomposition.

theorem sum_filtered_product_eq_sum_blocks {E : Type*} [AddCommMonoid E]
    (N U V : ℕ) (F : ℕ → ℕ → E) :
    (∑ d ∈ (Ioc U N ×ˢ Ioc V N).filter (fun d => d.1 * d.2 ≤ N), F d.1 d.2) =
      ∑ j ∈ range (Nat.log 2 N + 1), block N U V j F := by
…

Mentions: OAI.Problem337.F, OAI.Problem337.VaughanDyadic.block

theorem OAI.Problem337.VaughanDyadic.norm_hyperbola_le_sum_block_norms line 115

Source documentation

Triangle inequality with the actual dyadic block norms.

theorem norm_hyperbola_le_sum_block_norms {E : Type*} [SeminormedAddCommGroup E]
    (N U V : ℕ) (F : ℕ → ℕ → E) :
    ‖∑ m ∈ Ioc U N, ∑ n ∈ Ioc V (N / m), F m n‖ ≤
      ∑ j ∈ range (Nat.log 2 N + 1), ‖block N U V j F‖ := by
…

Mentions: OAI.Problem337.F, OAI.Problem337.VaughanDyadic.block

theorem OAI.Problem337.VaughanDyadic.norm_hyperbola_le_block_count line 123

Source documentation

Any genuine uniform block estimate pays only the number of dyadic blocks.

theorem norm_hyperbola_le_block_count {E : Type*} [SeminormedAddCommGroup E]
    (N U V : ℕ) (F : ℕ → ℕ → E) (B : ℝ)
    (hB : ∀ j < Nat.log 2 N + 1, ‖block N U V j F‖ ≤ B) :
    ‖∑ m ∈ Ioc U N, ∑ n ∈ Ioc V (N / m), F m n‖ ≤
      (Nat.log 2 N + 1 : ℕ) * B := by
…

Mentions: OAI.Problem337.F, OAI.Problem337.VaughanDyadic.block

theorem OAI.Problem337.VaughanDyadic.norm_hyperbola_le_log_budget line 136

Source documentation

Real-log normalization of the finite dyadic block count.

theorem norm_hyperbola_le_log_budget {E : Type*} [SeminormedAddCommGroup E]
    (N U V : ℕ) (F : ℕ → ℕ → E) (B : ℝ) (hB0 : 0 ≤ B)
    (hB : ∀ j < Nat.log 2 N + 1, ‖block N U V j F‖ ≤ B) :
    ‖∑ m ∈ Ioc U N, ∑ n ∈ Ioc V (N / m), F m n‖ ≤
      (1 + Real.log N / Real.log 2) * B := by
…

Mentions: OAI.Problem337.F, OAI.Problem337.VaughanDyadic.block