HyperbolaDyadicBridge.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.VaughanDyadic.block_eq_zero_of_large_base line 11
Source documentation
Empty high shells contribute nothing to the long--long hyperbola.
```
theorem block_eq_zero_of_large_base {E : Type*} [AddCommMonoid E]
    (N U V j : ℕ) (F : ℕ → ℕ → E) (hN : N < 2 ^ j * (V + 1)) :
    block N U V j F = 0 := by
…
```
Mentions: OAI.Problem337.F, OAI.Problem337.VaughanDyadic.block
theorem OAI.Problem337.VaughanDyadic.base_le_div_of_block_ne_zero line 25
Source documentation
Every nonzero block has row scale at most the hyperbolic long-column cap.
```
theorem base_le_div_of_block_ne_zero {E : Type*} [AddCommMonoid E]
    (N U V j : ℕ) (F : ℕ → ℕ → E) (hblock : block N U V j F ≠ 0) :
    2 ^ j ≤ N / (V + 1) := by
…
```
Mentions: OAI.Problem337.F, OAI.Problem337.VaughanDyadic.block
theorem OAI.Problem337.VaughanDyadic.shell_length_le line 33
Source documentation
The clipped contiguous shell has length at most its lower power-of-two scale.
```
theorem shell_length_le (N U j : ℕ) :
    min N (2 ^ (j + 1) - 1) + 1 - max (U + 1) (2 ^ j) ≤ 2 ^ j := by
…
```
theorem OAI.Problem337.VaughanDyadic.shell_card_le line 39

theorem OAI.Problem337.VaughanDyadic.phase_block_eq_columns line 45

Source documentation

The exact dyadic phase block is the column expression used by the hyperbolic correlation theorem, with no rectangular relaxation.

theorem phase_block_eq_columns (α : ℝ) (N U V j : ℕ) (a b : ℕ → ℂ) :
    block N U V j (fun m n =>
      a m * b n * HyperbolaCorrelation.phase (α * (m : ℝ) * (n : ℝ))) =
    ∑ m ∈ Finset.Icc (max (U + 1) (2 ^ j)) (min N (2 ^ (j + 1) - 1)),
      a m * ∑ n ∈ Finset.Ioc V (N / 2 ^ j),
        b n * HyperbolaCorrelation.column α N n m := by
…

Mentions: OAI.Problem337.VaughanDyadic.block, OAI.Problem337.HyperbolaCorrelation.phase, OAI.Problem337.HyperbolaCorrelation.column

theorem OAI.Problem337.VaughanDyadic.norm_phase_block_sq_le_energy line 63

Source documentation

A geometric row estimate at scale 2^j controls the actual dyadic block, retaining both coefficient energies and the moving hyperbolic endpoint.

theorem norm_phase_block_sq_le_energy
    (α : ℝ) (N U V j : ℕ) (a b : ℕ → ℂ) (C : ℝ)
    (hrow : ∀ n ∈ Finset.Ioc V (N / 2 ^ j),
      (∑ k ∈ Finset.Ioc V (N / 2 ^ j),
        VaughanBilinear.geometricBound (2 ^ j) (α * ((n : ℝ) - (k : ℝ)))) ≤ C) :
    ‖block N U V j (fun m n =>
      a m * b n * HyperbolaCorrelation.phase (α * (m : ℝ) * (n : ℝ)))‖ ^ 2 ≤
      (∑ m ∈ shell U N j, ‖a m‖ ^ 2) * C *
        (∑ n ∈ Finset.Ioc V (N / 2 ^ j), ‖b n‖ ^ 2) := by
…

Mentions: OAI.Problem337.VaughanBilinear.geometricBound, OAI.Problem337.VaughanDyadic.block, OAI.Problem337.HyperbolaCorrelation.phase, OAI.Problem337.VaughanDyadic.shell