VaughanIdentity.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Vaughan's identity with finite cutoffs

This file supplies an unconditional algebraic input to the analytic three-prime route. Multiplication of arithmetic functions below is Dirichlet convolution. No estimate for exponential sums over primes is assumed or asserted here.

def OAI.Problem337.Vaughan.shortPart line 20
Source documentation
The part of an arithmetic function supported on integers at most U.
```
def shortPart {R : Type*} [Zero R] (U : ℕ) (f : ArithmeticFunction R) :
    ArithmeticFunction R :=
…
```
def OAI.Problem337.Vaughan.longPart line 25
Source documentation
The complementary part, supported on integers strictly above U.
```
def longPart {R : Type*} [Zero R] (U : ℕ) (f : ArithmeticFunction R) :
    ArithmeticFunction R :=
…
```
lemma OAI.Problem337.Vaughan.shortPart_apply line 29
lemma OAI.Problem337.Vaughan.longPart_apply line 33
lemma OAI.Problem337.Vaughan.shortPart_add_longPart line 37
lemma OAI.Problem337.Vaughan.longPart_eq_sub_shortPart line 42

theorem OAI.Problem337.Vaughan.vonMangoldt_identity line 50

Source documentation

Vaughan's four-term identity, valid also at zero and for zero cutoffs. The first convolution is Type I; the second has a coefficient supported on [1,U*V]; the last is the long-long Type II convolution.

theorem vonMangoldt_identity (U V : ℕ) :
    ArithmeticFunction.vonMangoldt =
      shortPart V ArithmeticFunction.vonMangoldt +
      shortPart U (μ : ArithmeticFunction ℝ) * ArithmeticFunction.log -
      (shortPart U (μ : ArithmeticFunction ℝ) *
        shortPart V ArithmeticFunction.vonMangoldt) * (ζ : ArithmeticFunction ℝ) +
      (longPart U (μ : ArithmeticFunction ℝ) * (ζ : ArithmeticFunction ℝ)) *
        longPart V ArithmeticFunction.vonMangoldt := by
…

Mentions: OAI.Problem337.Vaughan.shortPart, OAI.Problem337.Vaughan.longPart

lemma OAI.Problem337.Vaughan.shortPart_mul_eq_zero_of_lt line 75
Source documentation
A convolution of two short parts has the expected product support.
```
lemma shortPart_mul_eq_zero_of_lt {R : Type*} [Semiring R]
    (U V n : ℕ) (f g : ArithmeticFunction R) (hn : U * V < n) :
    (shortPart U f * shortPart V g) n = 0 := by
…
```
Mentions: OAI.Problem337.Vaughan.shortPart
lemma OAI.Problem337.Vaughan.longPart_mul_eq_zero_of_le line 92
Source documentation
Convolving a long part cannot create a smaller positive index.
```
lemma longPart_mul_eq_zero_of_le {R : Type*} [Semiring R]
    (U n : ℕ) (f g : ArithmeticFunction R) (hn : n ≤ U) :
    (longPart U f * g) n = 0 := by
…
```
Mentions: OAI.Problem337.Vaughan.longPart
lemma OAI.Problem337.Vaughan.abs_shortPart_le line 103
lemma OAI.Problem337.Vaughan.abs_longPart_le line 107
lemma OAI.Problem337.Vaughan.abs_real_moebius_le_one line 111
def OAI.Problem337.Vaughan.typeICoefficient line 117
Source documentation
The short convolution coefficient appearing in Type I sums.
```
def typeICoefficient (U V : ℕ) : ArithmeticFunction ℝ :=
…
```
def OAI.Problem337.Vaughan.typeIICoefficient line 121
Source documentation
The coefficient appearing in the long-long Type II sum.
```
def typeIICoefficient (U : ℕ) : ArithmeticFunction ℝ :=
…
```
lemma OAI.Problem337.Vaughan.typeICoefficient_eq_zero line 124
lemma OAI.Problem337.Vaughan.typeIICoefficient_eq_zero line 127
lemma OAI.Problem337.Vaughan.abs_typeICoefficient_le_log line 131
Source documentation
The Type I coefficient costs only a logarithm, not a divisor function.
```
lemma abs_typeICoefficient_le_log (U V n : ℕ) :
    |typeICoefficient U V n| ≤ Real.log n := by
…
```
Mentions: OAI.Problem337.Vaughan.typeICoefficient
lemma OAI.Problem337.Vaughan.typeIICoefficient_apply line 156
lemma OAI.Problem337.Vaughan.abs_typeIICoefficient_le_divisors_card line 163
Source documentation
A uniform elementary coefficient bound for the Type II sum.
```
lemma abs_typeIICoefficient_le_divisors_card (U n : ℕ) :
    |typeIICoefficient U n| ≤ (n.divisors.card : ℝ) := by
…
```
Mentions: OAI.Problem337.Vaughan.typeIICoefficient