PublishedInputs.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Precisely stated published short-interval inputs

The short-interval estimates are formulated as hypotheses. The source is 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.

We use only natural length and outer cutoffs. Theorem 1.7 is stated in the weaker form needed by the application: a supplied lower bound on every pretentious distance in its specified range replaces their infimum. The frequency is fixed during the integral. No graph or correlation conclusion from the present manuscript is included among these published inputs.

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

theorem OAI.TwoPointCorrelations.UniformlyNonpretentious.bounded_moduli line 76

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/TwoPoint/PublishedInputs.lean:72 (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 96
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/TwoPoint/PublishedInputs.lean:92 (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 110
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/TwoPoint/PublishedInputs.lean:106 (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 129
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/TwoPoint/PublishedInputs.lean:125 (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