Documentation

LeanPool.NairTenenbaum.Hooley.Hooley

Hooley's divisor concentration function #

The definition in §1 and the coprime multiplication bound used to place it in the Nair–Tenenbaum class. Logarithmic windows are equivalent to the paper's exponential windows for positive divisors.

source
noncomputable def NairTenenbaum.divisorWindow (n : ℕ) (u : ℝ) :
ℕ

Number of divisors with logarithm in (u,u+1].

Equations
Instances For
    source
    noncomputable def NairTenenbaum.hooleyDelta (n : ℕ) :
    ℕ

    Hooley's Δ(n). The maximum exists since all window counts are natural numbers bounded by the number of divisors. We use Δ(0)=0.

    Equations
    Instances For
      source
      theorem NairTenenbaum.divisorWindow_le_card (n : ℕ) (u : ℝ) :
      divisorWindow n u ≤ n.divisors.card
      source
      theorem NairTenenbaum.divisorWindow_bddAbove (n : ℕ) :
      BddAbove (Set.range (divisorWindow n))
      source
      theorem NairTenenbaum.divisorWindow_le_delta (n : ℕ) (u : ℝ) :
      divisorWindow n u ≤ hooleyDelta n
      source
      theorem NairTenenbaum.hooleyDelta_le_card (n : ℕ) :
      hooleyDelta n ≤ n.divisors.card
      source
      theorem NairTenenbaum.hooleyDelta_attained (n : ℕ) :
      ∃ (u : ℝ), divisorWindow n u = hooleyDelta n
      source
      @[simp]
      theorem NairTenenbaum.hooleyDelta_zero :
      hooleyDelta 0 = 0
      source
      theorem NairTenenbaum.divisorWindow_eq_sum (n : ℕ) (u : ℝ) :
      divisorWindow n u = ∑ d ∈ n.divisors, if u < Real.log ↑d ∧ Real.log ↑d ≤ u + 1 then 1 else 0
      source
      theorem NairTenenbaum.sum_divisors_mul_of_coprime {m n : ℕ} (hmn : m.Coprime n) (f : ℕ → ℕ) :
      ∑ d ∈ (m * n).divisors, f d = ∑ a ∈ m.divisors, ∑ b ∈ n.divisors, f (a * b)
      source
      theorem NairTenenbaum.divisorWindow_mul {m n : ℕ} (hmn : m.Coprime n) (u : ℝ) :
      divisorWindow (m * n) u = ∑ a ∈ m.divisors, divisorWindow n (u - Real.log ↑a)

      Exact splitting of a divisor window over coprime factors.

      source
      theorem NairTenenbaum.hooleyDelta_mul_le {m n : ℕ} (hmn : m.Coprime n) :
      hooleyDelta (m * n) ≤ m.divisors.card * hooleyDelta n

      The multiplication bound stated in §1.

      source
      theorem NairTenenbaum.divisor_interval_le_delta {n : ℕ} {D E : ℝ} (hD : 0 < D) (hE : E ≤ Real.exp 1 * D) :
      {d ∈ n.divisors | D < ↑d ∧ ↑d ≤ E}.card ≤ hooleyDelta n

      An arbitrary logarithmic window dominates every shorter interval of divisors.

      source
      theorem NairTenenbaum.dyadic_divisors_le_delta {n : ℕ} {D : ℝ} (hD : 0 < D) :
      {d ∈ n.divisors | D < ↑d ∧ ↑d ≤ 2 * D}.card ≤ hooleyDelta n

      The pointwise dyadic divisor bound used in Corollary 5.