PublishedInputs.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Short-interval estimates for multiplicative functions

The estimates specialize K. Matomäki, M. Radziwiłł and T. Tao, An averaged form of Chowla's conjecture, Algebra & Number Theory 9 (2015), 2167–2196, corrected arXiv:1503.05121v3 (1 March 2022), Theorems 1.3 and 1.7; DOI 10.2140/ant.2015.9.2167.

The frequency is fixed during the integral. A uniform lower bound on the squared pretentious distances replaces the infimum in Theorem 1.7.

def OAI.TwoPointCorrelations.additiveCharacter line 26
Source documentation
The usual additive character e(αn) = exp(2πiαn).
Also declared: OAI/NumberTheory/TwoPointCorrelations/PublishedInputs.lean:30 (same declaration text).
```
noncomputable def additiveCharacter (α : ℝ) (n : ℕ) : ℂ :=
…
```
def OAI.TwoPointCorrelations.shortExponentialSum line 31
Source documentation
Sum over the integers y < n ≤ y+H (for the nonnegative starting points used in the integral).
Also declared: OAI/NumberTheory/TwoPointCorrelations/PublishedInputs.lean:35 (same declaration text).
```
noncomputable def shortExponentialSum (b : ℕ → ℂ) (H : ℕ) (α y : ℝ) : ℂ :=
…
```
def OAI.TwoPointCorrelations.shortExponentialIntegral line 36
Source documentation
The mean over interval origins, with a single fixed frequency.
Also declared: OAI/NumberTheory/TwoPointCorrelations/PublishedInputs.lean:40 (same declaration text).
```
noncomputable def shortExponentialIntegral (b : ℕ → ℂ) (X H : ℕ) (α : ℝ) : ℝ :=
…
```
def OAI.TwoPointCorrelations.mrtModulusCutoff line 40
Source documentation
The character-modulus cutoff in corrected MRT Theorem 1.7.
Also declared: OAI/NumberTheory/TwoPointCorrelations/PublishedInputs.lean:44 (same declaration text).
```
noncomputable def mrtModulusCutoff (X H : ℕ) : ℝ :=
…
```
def OAI.TwoPointCorrelations.mrtShortError line 44
Source documentation
The error shared by MRT Theorems 1.3 and 1.7.
Also declared: OAI/NumberTheory/TwoPointCorrelations/PublishedInputs.lean:48 (same declaration text).
```
noncomputable def mrtShortError (X H : ℕ) : ℝ :=
…
```
def OAI.TwoPointCorrelations.MRTDistanceLowerBound line 49
Source documentation
The exact range of lower bounds required by corrected MRT Theorem 1.7.
Also declared: OAI/NumberTheory/TwoPointCorrelations/PublishedInputs.lean:53 (same declaration text).
```
def MRTDistanceLowerBound (b : ℕ → ℂ) (X H : ℕ) (M : ℝ) : Prop :=
…
```
def OAI.TwoPointCorrelations.MRTShortExponentialInput line 56
Source documentation
Natural-cutoff specialization of corrected MRT Theorem 1.7, with an explicit lower bound M in place of the infimum of squared distances.
Also declared: OAI/NumberTheory/TwoPointCorrelations/PublishedInputs.lean:60 (same declaration text).
```
def MRTShortExponentialInput : Prop :=
…
```
def OAI.TwoPointCorrelations.MRTLiouvilleShortInput line 65
Source documentation
Natural-cutoff Liouville specialization of MRT Theorem 1.3. Endpoint conventions differ only at a measure-zero set of interval origins.
Also declared: OAI/NumberTheory/TwoPointCorrelations/PublishedInputs.lean:69 (same declaration text).
```
def MRTLiouvilleShortInput : Prop :=
…
```

theorem OAI.TwoPointCorrelations.UniformlyNonpretentious.bounded_moduli line 72

Source documentation

At a fixed modulus cutoff, uniform nonpretentiousness gives one bound simultaneously for every character and every permitted finite-prime change.

Also declared: OAI/NumberTheory/TwoPointCorrelations/PublishedInputs.lean:76 (same declaration text).

theorem UniformlyNonpretentious.bounded_moduli {f : ℕ → ℂ}
    (hfnp : UniformlyNonpretentious f) (hf : OneBounded f)
    (P : Finset ℕ) (Q : ℕ) (K : ℝ) :
    ∀ᶠ N : ℕ in Filter.atTop, ∀ q : ℕ, 0 < q → q ≤ Q →
      ∀ (χ : DirichletCharacter ℂ q) (b : ℕ → ℂ), OneBounded b →
        (∀ p, Nat.Prime p → p ∉ P → b p = f p) →
        ∀ t : ℝ, |t| ≤ (N : ℝ) → K ≤ squaredDistance b (characterTwist χ t) N := by
…

Mentions: OAI.TwoPointCorrelations.UniformlyNonpretentious, OAI.TwoPointCorrelations.OneBounded

theorem OAI.TwoPointCorrelations.UniformlyNonpretentious.eventually_mrt_lower_bound line 92
Source documentation
Fixing the short interval length leaves only finitely many moduli in the published theorem. Thus the entire MRT distance hypothesis holds uniformly.
Also declared: OAI/NumberTheory/TwoPointCorrelations/PublishedInputs.lean:96 (same declaration text).
```
theorem UniformlyNonpretentious.eventually_mrt_lower_bound {f : ℕ → ℂ}
    (hfnp : UniformlyNonpretentious f) (hf : OneBounded f)
    (P : Finset ℕ) (H : ℕ) (M : ℝ) :
    ∀ᶠ N : ℕ in Filter.atTop, ∀ b : ℕ → ℂ, OneBounded b →
      (∀ p, Nat.Prime p → p ∉ P → b p = f p) → MRTDistanceLowerBound b N H M := by
…
```
Mentions: OAI.TwoPointCorrelations.UniformlyNonpretentious, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.MRTDistanceLowerBound
theorem OAI.TwoPointCorrelations.MRTShortExponentialInput.normalized line 106
Source documentation
The published short-sum estimate immediately gives a bound on the normalized mean, without moving a frequency supremum into the integral.
Also declared: OAI/NumberTheory/TwoPointCorrelations/PublishedInputs.lean:110 (same declaration text).
```
theorem MRTShortExponentialInput.normalized (hMRT : MRTShortExponentialInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ (X H : ℕ), 10 ≤ H → H ≤ X →
      ∀ (b : ℕ → ℂ), Multiplicative b → OneBounded b →
        ∀ M : ℝ, MRTDistanceLowerBound b X H M → ∀ α : ℝ,
          shortExponentialIntegral b X H α / ((H : ℝ) * (X : ℝ)) ≤
            C * (Real.exp (-M / 20) + mrtShortError X H) := by
…
```
Mentions: OAI.TwoPointCorrelations.MRTShortExponentialInput, OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.MRTDistanceLowerBound, OAI.TwoPointCorrelations.shortExponentialIntegral, OAI.TwoPointCorrelations.mrtShortError
theorem OAI.TwoPointCorrelations.MRTShortExponentialInput.finite_prime_changes line 125
Source documentation
A genuine conditional consequence of published MRT Theorem 1.7: finite local modifications preserve the uniform short-sum estimate at every fixed short-interval length. The estimate is uniform over all modifications and frequencies, with the frequency still outside the integral.
Also declared: OAI/NumberTheory/TwoPointCorrelations/PublishedInputs.lean:129 (same declaration text).
```
theorem MRTShortExponentialInput.finite_prime_changes
    (hMRT : MRTShortExponentialInput) {f : ℕ → ℂ}
    (hfnp : UniformlyNonpretentious f) (hf : OneBounded f) (P : Finset ℕ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (H : ℕ), 10 ≤ H → ∀ M : ℝ,
      ∀ᶠ N : ℕ in Filter.atTop, ∀ b : ℕ → ℂ,
        Multiplicative b → OneBounded b →
        (∀ p, Nat.Prime p → p ∉ P → b p = f p) → ∀ α : ℝ,
          shortExponentialIntegral b N H α / ((H : ℝ) * (N : ℝ)) ≤
            C * (Real.exp (-M / 20) + mrtShortError N H) := by
…
```
Mentions: OAI.TwoPointCorrelations.MRTShortExponentialInput, OAI.TwoPointCorrelations.UniformlyNonpretentious, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.shortExponentialIntegral, OAI.TwoPointCorrelations.mrtShortError