DensityCRTProduct.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Constructing the density product and its Fourier hypotheses

structure OAI.Ostmann.DensityCRTData line 13
Source documentation
A bounded density product with its proved local-mean-zero consequence.
```
structure DensityCRTData (q : ℕ) [NeZero q] where
…
```
def OAI.Ostmann.DensityCRTData.one line 20
def OAI.Ostmann.DensityCRTData.prime line 27
def OAI.Ostmann.DensityCRTData.mul line 34
theorem OAI.Ostmann.prime_list_prod_pos line 45
def OAI.Ostmann.densityCRTList line 54
Source documentation
This is the actual product of the centered functions, formed by CRT along the list of distinct prime factors.
```
noncomputable def densityCRTList (ps : List ℕ) (hp : ∀ p ∈ ps, p.Prime)
    (hc : ps.Pairwise Nat.Coprime) (S : ∀ p : ℕ, Finset (ZMod p)) :
    @DensityCRTData ps.prod ⟨(prime_list_prod_pos ps hp).ne'⟩ := by
…
```
Mentions: OAI.Ostmann.DensityCRTData, OAI.Ostmann.prime_list_prod_pos
theorem OAI.Ostmann.densityCRTList_intCast line 68

theorem OAI.Ostmann.densityCRTList_energy line 92

Source documentation

The hypotheses of the small-kernel bound hold for the original finite product of centered density functions.

theorem densityCRTList_energy (ps : List ℕ) (hp : ∀ p ∈ ps, p.Prime)
    (hc : ps.Pairwise Nat.Coprime) (S : ∀ p : ℕ, Finset (ZMod p)) :
    let : NeZero ps.prod := ⟨(prime_list_prod_pos ps hp).ne'⟩
…

Mentions: OAI.Ostmann.prime_list_prod_pos

theorem OAI.Ostmann.densityCRT_small_quadratic_sum line 101

Source documentation

The manuscript's small-kernel bound with all density Fourier hypotheses supplied by the original centered factors.

theorem densityCRT_small_quadratic_sum (ps : List ℕ) (hp : ∀ p ∈ ps, p.Prime)
    (hc : ps.Pairwise Nat.Coprime) (S : ∀ p : ℕ, Finset (ZMod p))
    (W : ℕ) (a : ZMod ps.prod) (weight : ℕ → ℂ) (B C N : ℝ)
    (hB : 0 ≤ B) (hN : 0 < N) (hq : (ps.prod : ℝ) ≤ N)
    (hW : (W : ℝ) ≤ C * N) (hw : ∀ w ∈ Finset.Ioc 0 W, ‖weight w‖ ≤ B) :
    let : NeZero ps.prod := ⟨(prime_list_prod_pos ps hp).ne'⟩
…

Mentions: OAI.Ostmann.prime_list_prod_pos