VaughanHyperbola.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Finite hyperbola reindexing for Vaughan sums

An exact finite change of variables from n = a*b to pairs of positive integers below a hyperbola. The arbitrary weight version is suitable for both rational additive characters and real-frequency exponential sums.

def OAI.Problem337.Vaughan.hyperbola line 19
Source documentation
Positive lattice points below the multiplicative hyperbola a*b ≤ N.
```
def hyperbola (N : ℕ) : Finset (ℕ × ℕ) :=
…
```
lemma OAI.Problem337.Vaughan.mem_hyperbola line 22
theorem OAI.Problem337.Vaughan.sum_divisor_fibers line 41
Source documentation
The divisor-antidiagonal fibers partition the positive hyperbola exactly. The summand may also depend on the product index n.
```
theorem sum_divisor_fibers {A : Type*} [AddCommMonoid A]
    (N : ℕ) (F : ℕ → ℕ → ℕ → A) :
    (∑ n ∈ Finset.Icc 1 N, ∑ ab ∈ n.divisorsAntidiagonal, F n ab.1 ab.2) =
      ∑ ab ∈ hyperbola N, F (ab.1 * ab.2) ab.1 ab.2 := by
…
```
Mentions: OAI.Problem337.F, OAI.Problem337.Vaughan.hyperbola
theorem OAI.Problem337.Vaughan.sum_hyperbola_eq_nested line 78
Source documentation
The hyperbola sum as ordinary nested integer intervals. The inner endpoint is the natural-number quotient N / a; the outer interval excludes zero.
```
theorem sum_hyperbola_eq_nested {A : Type*} [AddCommMonoid A]
    (N : ℕ) (F : ℕ → ℕ → A) :
    (∑ ab ∈ hyperbola N, F ab.1 ab.2) =
      ∑ a ∈ Finset.Icc 1 N, ∑ b ∈ Finset.Icc 1 (N / a), F a b := by
…
```
Mentions: OAI.Problem337.F, OAI.Problem337.Vaughan.hyperbola
theorem OAI.Problem337.Vaughan.sum_convolution_hyperbola line 114
Source documentation
Exact finite convolution reindexing with an arbitrary multiplicative weight. No convergence or support hypotheses on the weight are needed.
```
theorem sum_convolution_hyperbola {R : Type*} [Semiring R]
    (N : ℕ) (f g : ArithmeticFunction R) (w : ℕ → R) :
    (∑ n ∈ Finset.Icc 1 N, (f * g) n * w n) =
      ∑ ab ∈ hyperbola N, (f ab.1 * g ab.2) * w (ab.1 * ab.2) := by
…
```
Mentions: OAI.Problem337.Vaughan.hyperbola

theorem OAI.Problem337.Vaughan.sum_real_convolution_hyperbola line 123

Source documentation

Real arithmetic coefficients with complex weights, the combination used for the von-Mangoldt exponential sum.

theorem sum_real_convolution_hyperbola
    (N : ℕ) (f g : ArithmeticFunction ℝ) (w : ℕ → ℂ) :
    (∑ n ∈ Finset.Icc 1 N, ((f * g) n : ℂ) * w n) =
      ∑ ab ∈ hyperbola N, ((f ab.1 * g ab.2 : ℝ) : ℂ) * w (ab.1 * ab.2) := by
…

Mentions: OAI.Problem337.Vaughan.hyperbola

theorem OAI.Problem337.Vaughan.sum_real_convolution_eq_nested line 131

Source documentation

The traditional nested-interval form of the finite convolution identity.

theorem sum_real_convolution_eq_nested
    (N : ℕ) (f g : ArithmeticFunction ℝ) (w : ℕ → ℂ) :
    (∑ n ∈ Finset.Icc 1 N, ((f * g) n : ℂ) * w n) =
      ∑ a ∈ Finset.Icc 1 N, ∑ b ∈ Finset.Icc 1 (N / a),
        ((f a * g b : ℝ) : ℂ) * w (a * b) := by
…