OAI/NumberTheory/Ostmann/ZeroDensity/OriginalDensityCorrelation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.prime_list_nodup line 11
2. def OAI.Ostmann.supportCorrelationSide line 22
3. theorem OAI.Ostmann.prod_mask_subset line 25
4. theorem OAI.Ostmann.local_correlation_product line 30
5. theorem OAI.Ostmann.original_density_correlation_model line 51

   Source documentation

   Both original transforms have one common periodic model. Its coefficient bound is derived from the local density functions, including their CRT twists.

   theorem original_density_correlation_model (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)
       (vp : (ZMod ps.prod)ˣ) (vq : (ZMod qs.prod)ˣ)
       (f : ∀ p : ℕ, ZMod p → ℂ) (hf : ∀ p ∈ rs, ∀ x, ‖f p x‖ ≤ 1) :
       let : NeZero ps.prod := ⟨(prime_list_prod_pos ps hp).ne'⟩
   …

   Mentions: OAI.Ostmann.prime_list_prod_pos

6. theorem OAI.Ostmann.original_density_correlation_weighted_bound line 81

   Source documentation

   The weighted periodic estimate applies to the two CRT divisor transforms.

   theorem original_density_correlation_weighted_bound (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)
       (vp : (ZMod ps.prod)ˣ) (vq : (ZMod qs.prod)ˣ)
       (f : ∀ p : ℕ, ZMod p → ℂ) (hf : ∀ p ∈ rs, ∀ x, ‖f p x‖ ≤ 1)
       (α : ℝ) (w : ℕ → ℂ) (N : ℕ) :
       let : NeZero ps.prod := ⟨(prime_list_prod_pos ps hp).ne'⟩
   …

   Mentions: OAI.Ostmann.prime_list_prod_pos