PrimeCRTFourier.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Multiplying the local correlation bounds over the prime factors

def OAI.Ostmann.primeCRTFunction line 13

Source documentation

The actual function on the product modulus obtained from local prime functions.

noncomputable def primeCRTFunction (ps : List ℕ) (hp : ∀ p ∈ ps, p.Prime)
    (hc : ps.Pairwise Nat.Coprime) (F : ∀ p : ℕ, ZMod p → ℂ) : ZMod ps.prod → ℂ := by
…

theorem OAI.Ostmann.primeCRTFunction_intCast line 23

theorem OAI.Ostmann.primeCRTFunction_coefficient_le line 41

Source documentation

Probability-normalized Fourier coefficients multiply under CRT.

theorem primeCRTFunction_coefficient_le (ps : List ℕ) (hp : ∀ p ∈ ps, p.Prime)
    (hc : ps.Pairwise Nat.Coprime) (F : ∀ p : ℕ, ZMod p → ℂ) (A : ℕ → ℝ)
    (hA : ∀ p ∈ ps, 0 ≤ A p)
    (hF : ∀ p (h : p ∈ ps), ∀ u : ZMod p, ‖@additiveFourier p ⟨(hp p h).ne_zero⟩ (F p) u‖ ≤ A p) :
    let : NeZero ps.prod := ⟨(prime_list_prod_pos ps hp).ne'⟩
…

Mentions: OAI.Ostmann.additiveFourier, OAI.Ostmann.prime_list_prod_pos

theorem OAI.Ostmann.weighted_periodic_linear_long_bound line 71

Source documentation

A dyadic interval long compared with the period absorbs the Fourier-grid loss.

theorem weighted_periodic_linear_long_bound (q : ℕ) [NeZero q]
    (f : ZMod q → ℂ) (A α : ℝ) (hA : 0 ≤ A)
    (hf : ∀ u, ‖additiveFourier f u‖ ≤ A) (w : ℕ → ℂ) (N : ℕ)
    (hN : (q : ℝ) * (1 + Real.log q) ≤ N) :
    ‖∑ n ∈ Finset.range N, w n * (f (n : ZMod q) * realAdditivePhase α ^ n)‖ ≤
      discreteVariation w N * (4 * A * N) := by
…

Mentions: OAI.Ostmann.additiveFourier, OAI.Ostmann.realAdditivePhase, OAI.Ostmann.discreteVariation