OAI/NumberTheory/TwoPoint/Halasz/HalaszIntegerWindow.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Counting lattice points near integers, with all interval endpoints real.

  1. lemma OAI.TwoPointCorrelations.halasz_integer_interval_card line 12
  2. theorem OAI.TwoPointCorrelations.halasz_integer_window_card line 30

    Source documentation

    A finite set of integers lying in [-K,K] whose multiples by γ are close to integers. This is the lattice count used by the double mean-value method.

    theorem halasz_integer_window_card (S : Finset ℤ) {K γ δ : ℝ}
    (hK : 0≤K) (hγ : 0<γ) (hδ : 0≤δ) (hδhalf : δ≤1/2)
    (hS : ∀ d∈S, |(d:ℝ)|≤K ∧ ‖((γ*(d:ℝ):ℝ):AddCircle (1:ℝ))‖≤δ) :
    (S.card:ℝ)≤4*K*δ+2*K*γ+4*δ/γ+2 := by
…