DensityCorrelation.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The prime-by-prime correlation bound for centered densities

inductive OAI.Ostmann.CorrelationSide line 12
Source documentation
Which of the two squarefree divisors contains a prime of their union.
```
inductive CorrelationSide where
…
```
def OAI.Ostmann.primeDensityFourier line 19
Source documentation
Extend the local transform to an unrestricted prime index. The value at zero is immaterial; all applications index positive primes.
```
noncomputable def primeDensityFourier (f : ∀ p : ℕ, ZMod p → ℂ) (p : ℕ) : ZMod p → ℂ :=
…
```
theorem OAI.Ostmann.primeDensityFourier_eq line 22
def OAI.Ostmann.correlationPrimeFactor line 26
def OAI.Ostmann.correlationPrimeBound line 34
theorem OAI.Ostmann.correlationPrimeBound_nonneg line 40
theorem OAI.Ostmann.correlationPrimeFactor_coefficient_le line 45

theorem OAI.Ostmann.density_correlation_coefficient_bound line 64

Source documentation

This proves the local-product form of the manuscript's A_{d,d'}, with no analytic hypothesis on the density beyond its pointwise bound.

theorem density_correlation_coefficient_bound (ps : List ℕ)
    (hp : ∀ p ∈ ps, p.Prime) (hc : ps.Pairwise Nat.Coprime)
    (f : ∀ p : ℕ, ZMod p → ℂ) (hf : ∀ p ∈ ps, ∀ x, ‖f p x‖ ≤ 1)
    (side : ℕ → CorrelationSide) (a b : ∀ p : ℕ, (ZMod p)ˣ) :
    let : NeZero ps.prod := ⟨(prime_list_prod_pos ps hp).ne'⟩
…

Mentions: OAI.Ostmann.CorrelationSide, OAI.Ostmann.prime_list_prod_pos

theorem OAI.Ostmann.density_correlation_weighted_sum_bound line 80

Source documentation

The weighted linear-phase estimate for the actual product of local correlation factors.

theorem density_correlation_weighted_sum_bound (ps : List ℕ)
    (hp : ∀ p ∈ ps, p.Prime) (hc : ps.Pairwise Nat.Coprime)
    (f : ∀ p : ℕ, ZMod p → ℂ) (hf : ∀ p ∈ ps, ∀ x, ‖f p x‖ ≤ 1)
    (side : ℕ → CorrelationSide) (a b : ∀ p : ℕ, (ZMod p)ˣ)
    (α : ℝ) (w : ℕ → ℂ) (N : ℕ) :
    ‖∑ n ∈ Finset.range N, w n *
      (primeCRTFunction ps hp hc (correlationPrimeFactor f side a b) (n : ZMod ps.prod) *
        realAdditivePhase α ^ n)‖ ≤
      discreteVariation w N * (2 * (ps.map (correlationPrimeBound side)).prod *
        ((N : ℝ) + ps.prod * (1 + Real.log ps.prod))) := by
…

Mentions: OAI.Ostmann.CorrelationSide, OAI.Ostmann.primeCRTFunction, OAI.Ostmann.correlationPrimeFactor, OAI.Ostmann.realAdditivePhase, OAI.Ostmann.discreteVariation, OAI.Ostmann.correlationPrimeBound