PublishedInputs.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Published short-interval inputs for the joint Dickman problem

These definitions are propositions to be supplied as hypotheses. They are not axioms or proofs of the cited analytic theorems. In particular they do not assume joint independence at the shift one, the manuscript's new mixed decorrelation proposition, or any of its graph estimates.

The natural-number floor is harmless here: all intervals to which the inputs apply have positive left endpoint. Finset.Ioc implements the convention z < n ≤ z + H; changing the inclusion of the endpoints has the elementary O(1 / H) cost recorded in the manuscript.

def OAI.JointDickman.PublishedInputs.realShortAverage line 29
Source documentation
A real short average, with the manuscript's open-left endpoint convention.
```
noncomputable def realShortAverage (f : ArithmeticFunction ℝ) (H z : ℝ) : ℝ :=
…
```
def OAI.JointDickman.PublishedInputs.complexShortAverage line 33
Source documentation
A complex short average with the same endpoint convention.
```
noncomputable def complexShortAverage (f : ArithmeticFunction ℂ) (H z : ℝ) : ℂ :=
…
```
def OAI.JointDickman.PublishedInputs.realLongAverage line 37
Source documentation
The mean on the dyadic interval (X, 2X].
```
noncomputable def realLongAverage (f : ArithmeticFunction ℝ) (X : ℝ) : ℝ :=
…
```
def OAI.JointDickman.PublishedInputs.RealShortIntervalInput line 47
Source documentation
The mean-square comparison needed from Matomäki and Radziwiłł, Multiplicative functions in short intervals, Ann. of Math. 183 (2016), Theorem 1, DOI 10.4007/annals.2016.183.3.6, arXiv:1501.04585v4.
Theorem 1 is uniform in the multiplicative function, interval length, and exceptional-set tolerance. Its uniform exceptional-set bound and boundedness give this mean-square consequence (manuscript Theorem labels-real-MR).
```
def RealShortIntervalInput : Prop :=
…
```
def OAI.JointDickman.PublishedInputs.primeDistanceSquared line 57
Source documentation
The squared pretentious distance from n ↦ n^(it) up to X.
```
noncomputable def primeDistanceSquared (f : ArithmeticFunction ℂ) (X t : ℝ) : ℝ :=
…
```
def OAI.JointDickman.PublishedInputs.minimumDistance line 63
Source documentation
The minimum squared distance over the frequency interval [-X, X].
```
noncomputable def minimumDistance (f : ArithmeticFunction ℂ) (X : ℝ) : ℝ :=
…
```
def OAI.JointDickman.PublishedInputs.ComplexShortIntervalInput line 74
Source documentation
The quantitative complex short-average input from Matomäki, Radziwiłł, and Tao, An averaged form of Chowla's conjecture, Algebra & Number Theory 9 (2015), Theorem A.1, DOI 10.2140/ant.2015.9.2167.
The source is the corrected arXiv:1503.05121v3 (1 March 2022); the correction after Proposition A.3 permits exp (-M). The weaker (1 + M) * exp (-M) used here is the manuscript's Theorem labels-complex-MRT and also covers small M. The absolute implied constant is represented by C.
```
def ComplexShortIntervalInput : Prop :=
…
```