RoughConvolution.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Exact removal of the small prime factors

Removing a finite set of prime factors is an exact convolution identity. The moving roughness cutoff is then controlled by Selberg–Delange estimates.

def OAI.JointDickman.squarefreeWeight line 21
Source documentation
The squarefree coefficient μ(n)^2 z^ω(n). On squarefree integers, the number of prime factors with multiplicity equals the number of distinct prime factors.
```
noncomputable def squarefreeWeight (z : ℝ) : ArithmeticFunction ℝ :=
…
```
theorem OAI.JointDickman.squarefreeWeight_one line 24
theorem OAI.JointDickman.squarefreeWeight_isMultiplicative line 27
def OAI.JointDickman.smoothCorrection line 36
Source documentation
The finite Euler-factor inverse supported on integers whose prime factors all belong to the excluded set.
```
noncomputable def smoothCorrection (E : Finset ℕ) (z : ℝ) : ArithmeticFunction ℝ :=
…
```
theorem OAI.JointDickman.smoothCorrection_one line 40
theorem OAI.JointDickman.smoothCorrection_isMultiplicative line 43
def OAI.JointDickman.roughSquarefreeWeight line 52
Source documentation
Restriction to integers with no prime factor from E.
```
noncomputable def roughSquarefreeWeight (E : Finset ℕ) (z : ℝ) : ArithmeticFunction ℝ :=
…
```
theorem OAI.JointDickman.roughSquarefreeWeight_one line 55
theorem OAI.JointDickman.roughSquarefreeWeight_isMultiplicative line 58
theorem OAI.JointDickman.squarefreeWeight_prime_pow line 66
theorem OAI.JointDickman.smoothCorrection_prime_pow line 75
theorem OAI.JointDickman.roughSquarefreeWeight_prime_pow line 82

theorem OAI.JointDickman.squarefreeWeight_convolution_prime_pow line 90

Source documentation

Only the divisors 1 and p contribute from the squarefree weight.

theorem squarefreeWeight_convolution_prime_pow (z : ℝ) (h : ArithmeticFunction ℝ)
    {p k : ℕ} (hp : p.Prime) (hk : k ≠ 0) :
    (squarefreeWeight z * h) (p ^ k) = h (p ^ k) + z * h (p ^ (k - 1)) := by
…

Mentions: OAI.JointDickman.squarefreeWeight

theorem OAI.JointDickman.squarefreeWeight_mul_smoothCorrection line 104
Source documentation
Removing finitely many Euler factors is exact at every integer.
```
theorem squarefreeWeight_mul_smoothCorrection (E : Finset ℕ) (z : ℝ) :
    squarefreeWeight z * smoothCorrection E z = roughSquarefreeWeight E z := by
…
```
Mentions: OAI.JointDickman.squarefreeWeight, OAI.JointDickman.smoothCorrection, OAI.JointDickman.roughSquarefreeWeight
theorem OAI.JointDickman.roughSquarefreeWeight_summatory line 131
Source documentation
Exact finite summatory identity used before the analytic truncation.
```
theorem roughSquarefreeWeight_summatory (E : Finset ℕ) (z : ℝ) (N : ℕ) :
    (∑ n ∈ Ioc 0 N, roughSquarefreeWeight E z n) =
      ∑ v ∈ Ioc 0 N, smoothCorrection E z v *
        ∑ m ∈ Ioc 0 (N / v), squarefreeWeight z m := by
…
```
Mentions: OAI.JointDickman.roughSquarefreeWeight, OAI.JointDickman.smoothCorrection, OAI.JointDickman.squarefreeWeight