HalaszWindowPairCount.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Nearby pairs of moment frequencies are controlled by the zero moment and a product of one-dimensional near-integer counts.

def OAI.TwoPointCorrelations.halaszIntegerWindow line 14
lemma OAI.TwoPointCorrelations.halasz_integer_window_size line 17
lemma OAI.TwoPointCorrelations.halasz_integer_window_trivial line 27
theorem OAI.TwoPointCorrelations.halasz_near_pair_count line 40

theorem OAI.TwoPointCorrelations.halasz_near_pair_count_abs line 80

Source documentation

The lattice count depends only on the absolute coefficient; alternating Taylor signs therefore incur no additional factor.

theorem halasz_near_pair_count_abs {ι : Type*} [Fintype ι] {k : ℕ}
    (f : ι → Fin k → ℤ) (L : Fin k → ℕ) (γ δ : Fin k → ℝ)
    (hγ : ∀ j,γ j≠0) (hδ : ∀ j,0≤δ j) (hδquarter : ∀ j,δ j≤1/4)
    (hdiff : ∀ x y j, |f x j-f y j|≤(L j:ℤ)) :
    ((univ.filter (fun xy : ι×ι => HalaszWindowNear δ
      (halaszScaledFrequency γ (f xy.1)) (halaszScaledFrequency γ (f xy.2)))).card:ℝ)≤
      (halaszRepresentationCount f 0:ℝ)*
        ∏ j,min (2*(L j:ℝ)+1)
          (8*(L j:ℝ)*δ j+2*L j* |γ j| +8*δ j/ |γ j| +2) := by
…

Mentions: OAI.TwoPointCorrelations.HalaszWindowNear, OAI.TwoPointCorrelations.halaszScaledFrequency, OAI.TwoPointCorrelations.halaszRepresentationCount