OAI/NumberTheory/Ostmann/QuadraticCenter/TruncatedQuadraticCorrelation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.densityWave line 12
2. def OAI.Ostmann.normalizedDensityWaveSum line 16
3. theorem OAI.Ostmann.truncated_quadratic_correlation_bound line 24

   Source documentation

   The normalized large-kernel correlation estimate, with the finite support pair count and the two smooth scaling bounds made explicit.

   theorem truncated_quadratic_correlation_bound {ι κ : Type*}
       (ps qs rs : List ℕ)
       (hp : ∀ p ∈ ps, p.Prime) (hq : ∀ p ∈ qs, p.Prime) (hr : ∀ p ∈ rs, p.Prime)
       (hcp : ps.Pairwise Nat.Coprime) (hcq : qs.Pairwise Nat.Coprime) (hcr : rs.Pairwise Nat.Coprime)
       (hrs : rs.toFinset = ps.toFinset ∪ qs.toFinset)
       (f : ∀ p : ℕ, ZMod p → ℂ) (hf : ∀ p ∈ rs, ∀ x, ‖f p x‖ ≤ 1)
       (W : Finset ι) (V : Finset κ) (u : ι → (ZMod ps.prod)ˣ) (v' : κ → (ZMod qs.prod)ˣ)
       (Φ Ψ : 𝓢(ℝ, ℂ)) (α Y : ι → ℝ) (β Z : κ → ℝ)
       (R v C D H : ℝ) (M N : ℕ) (hR : 0 < R) (hv : 0 < v)
       (hC : 0 ≤ C) (hD : 0 ≤ D) (hM : 0 < M) (hN : 0 < N)
       (hperiod : rs.prod ^ 2 ≤ N)
       (hY : ∀ w ∈ W, 0 < Y w) (hZ : ∀ z ∈ V, 0 < Z z)
   …